projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cf36673) | patch
Reset built model flag at presolve in nonlinear (#5386)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 3 Nov 2020 18:17:32 +0000 (12:17 -0600)
committerGitHub <noreply@github.com>
Tue, 3 Nov 2020 18:17:32 +0000 (12:17 -0600)
commite2aff722e0b1072e90bd0c77e7030957364283cc
treefe19793d03140f173caabe3c5a1c9cf833e38ebbtree
parentcf36673d216949bb4306964c81488df3eb42b0c2commit | diff
Reset built model flag at presolve in nonlinear (#5386)

Fixes a bug in incremental with non-linear where the built model flag would still be true on the first call to check in a 2nd call to check-sat in incremental mode. This occurs when we are under the same SAT context when the model was built (likely level 0) on the subsequent check-sat call.

Fixes #5372
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/nl/issue5372-2-no-m-presolve.smt2 [new file with mode: 0644] blob