diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 16:39:39 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-26 16:39:39 -0600 |
commit | 8e476f1efeb7f8b3188ea1795ccd27f98f41e4d2 (patch) | |
tree | 518e5e881b33aa2fdaa409aa03a814713a43b69b /test | |
parent | 2405b98feeed522d7304207280591a71ee6c319a (diff) |
Use side effect utility for non-linear lemmas (#3780)
Fixes #3647.
Previously, when doing incremental linearization for transcedental functions, we would add points to the list of secant points at the time when linearization lemmas were generated. However, our strategy has been updated such that lemmas may be abandoned (say in the case that a higher priority lemma is found). Thus, our list of secant points had spurious points corresponding to lemmas that weren't sent. This led to assertion failures, and likely led to gaps in our linearization, hindering our ability to say sat/unsat.
This PR introduces a "lemma side effect" class to ensure that modifications to the state of the nonlinear solver are in sync with the lemmas we send out.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/nl/issue3647.smt2 | 6 |
2 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1113717ce..81540b160 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1311,6 +1311,7 @@ set(regress_1_tests regress1/nl/issue3300-approx-sqrt-witness.smt2 regress1/nl/issue3441.smt2 regress1/nl/issue3617.smt2 + regress1/nl/issue3647.smt2 regress1/nl/issue3656.smt2 regress1/nl/metitarski-1025.smt2 regress1/nl/metitarski-3-4.smt2 diff --git a/test/regress/regress1/nl/issue3647.smt2 b/test/regress/regress1/nl/issue3647.smt2 new file mode 100644 index 000000000..0fc0f55f9 --- /dev/null +++ b/test/regress/regress1/nl/issue3647.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-check-models --produce-models --decision=internal +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(assert (distinct (sin 1.0) 0.0)) +(check-sat) |