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

Timeout in model generation should not prevent a result #704

Closed
bclement-ocp opened this issue Jun 27, 2023 · 0 comments · Fixed by #722
Closed

Timeout in model generation should not prevent a result #704

bclement-ocp opened this issue Jun 27, 2023 · 0 comments · Fixed by #722
Assignees
@bclement-ocp
Milestone
2.5.0

Comments

@bclement-ocp
Copy link
Collaborator 

dune exec --release -- alt-ergo --frontend=legacy --sat-solver=Tableaux --interpretation=last -t 2 -o smtlib2 tests/arith/testfile-arith028.ae 
Done: 99% (873/875, 2 left) (jobs: 1)[FunSat]
 It seems that no model has been computed so far.
You may need to change your model generation strategy
or to increase your timeout.

; [Warning] Timeout
;

This should be unknown, not timeout (also the smtlib2 output option is not respected).
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Jun 27, 2023
@bclement-ocp
Add produce-models
404f772 
There are regressions otherwise, see OCamlPro#704
@bclement-ocp bclement-ocp added this to the 2.5.0 milestone Jun 27, 2023
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Jul 3, 2023
@bclement-ocp
Display "timeout" result even if timeout occurs in model generation
af4fea5 
Fixes OCamlPro#704

Note that this doesn't really fix the issue with smtlib2
tests/arith/testfile-arith028.ae because we display "timeout" instead of
"unknown", but at least we respect the output format now.
@bclement-ocp bclement-ocp mentioned this issue Jul 3, 2023
Merged
@bclement-ocp bclement-ocp self-assigned this Jul 3, 2023
bclement-ocp added a commit that referenced this issue Jul 10, 2023
@bclement-ocp
Display "timeout" result even if timeout occurs in model generation (#…
6a9a63e 
…722)

Fixes #704

Note that this doesn't really fix the issue with smtlib2
tests/arith/testfile-arith028.ae because we display "timeout" instead of
"unknown", but at least we respect the output format now.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@bclement-ocp bclement-ocp

Labels
None yet
Projects
None yet
Milestone
2.5.0
Development

Successfully merging a pull request may close this issue.

Display "timeout" result even if timeout occurs in model generation bclement-ocp/alt-ergo
1 participant
@bclement-ocp