-
Notifications
You must be signed in to change notification settings - Fork 1.5k
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.
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
[Consolidated 2] Issues related to tactic.default_tactic=smt sat.euf=true #5215
Comments
src/sat/smt/bv_invariant.cpp:98
|
src/sat/smt/euf_model.cpp:204
|
Nondet src/util/vector.h:484
|
ast.h:495
|
Memory leak
A stack with allocation locations would be greatly appreciated. |
src/sat/smt/bv_invariant.cpp:103
|
Nondet src/math/lp/lar_solver.cpp:1183
|
src/ast/euf/euf_egraph.cpp:294
|
src/sat/smt/euf_solver.cpp:367
|
As I wrote in the other bug: please don't file yet with :sat.threads or parallel.enable. These bugs often already manifest without threads, and if they only manifest with threads they are harder to debug. There is a different time to worry about multi-threaded behavior for the new code (the bugs would be around how constraints are copied). |
Threads are now disabled when using euf |
Commit 0422b59 |
|
|
All bugs marked by "eyes" are addressed. |
Invalid model
The text was updated successfully, but these errors were encountered: