Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Crash on model output from FMB - sorts? #461

Open
MichaelRawson opened this issue Jul 18, 2023 · 1 comment
Open

Crash on model output from FMB - sorts? #461

MichaelRawson opened this issue Jul 18, 2023 · 1 comment
Assignees
@selig @ibnyusuf

Comments

@MichaelRawson
Copy link
Contributor

Reported by Geoff from CASC-29.

If you run current master with --decode fmb+10_1_bce=on:fmbas=function:fmbsr=1.2:fde=unused:nm=0_846 ITP383_10.p we get a crash during model printing here where the item doesn't exist in the map. Debug build is fine.
@MichaelRawson
Copy link
Contributor Author

Original report was

I see that Vampire didn't manage to output a model for three problems in
the TFN division ...
ITP383_10 - https://www.tptp.org/CASC/29/WWWFiles/Results/TFN/Vampire-SAT---4.8/ITP383_10
ITP391_1 - https://www.tptp.org/CASC/29/WWWFiles/Results/TFN/Vampire-SAT---4.8/ITP391_1
ITP389_1 - https://www.tptp.org/CASC/29/WWWFiles/Results/TFN/Vampire-SAT---4.8/ITP389_1

It looks like it established that a finite model exists, but could not
get it out, right? Any comment (for the CASC report)?

@quickbeam123 quickbeam123 mentioned this issue May 30, 2024
Open
@quickbeam123 quickbeam123 mentioned this issue Jun 10, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@selig selig

@ibnyusuf ibnyusuf

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@selig @MichaelRawson @ibnyusuf