diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-10 10:06:27 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-10 16:06:27 +0000 |
| commit | cdcdd49a79ba03966cbb29c4f380f426c95a7d3a (patch) | |
| tree | de8cf667daead76fa107e8513c2a7915435d2473 /test/regress/regress1 | |
| parent | 2ff196ccba2ce611fe7320ef775955c291d34dab (diff) | |
Fix term registration and non-theory-preprocessed terms in substitutions (#6080)
This fixes two issues for preprocessing:
(1) The term preregistration visitor was calling preRegister on terms multiple times in a SAT context, which the linear arithmetic solver is sensitive to.
(2) It was possible for non-preprocessed terms to appear in assertions if they were on the RHS of substitutions learned by non-clausal simplification, and substituted into assertions post-theory-preprocessing.
To fix (1), the SharedTermsVisitor is update to track which theories has preregistered each term, as is done in the PreRegisterVisitor. To fix (2), we no longer apply-subst after theory preprocessing.
These two fixes are required to fix #6071.
Note: we should performance test this on SMT-LIB.
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/strings/issue6071-arith-prereg-i.smt2 | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/issue6071-arith-prereg-i.smt2 b/test/regress/regress1/strings/issue6071-arith-prereg-i.smt2 new file mode 100644 index 000000000..13fcaf428 --- /dev/null +++ b/test/regress/regress1/strings/issue6071-arith-prereg-i.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: -i +; EXPECT: sat +(set-logic ALL) +(set-option :strings-lazy-pp false) +(declare-fun ufbi4 (Bool Bool Bool Bool) Int) +(declare-fun str0 () String) +(declare-fun str8 () String) +(declare-fun i16 () Int) +(assert (= (str.to_int str0) (ufbi4 false true false (= 0 i16)))) +(push) +(assert (= str8 (str.from_int (str.to_int str0)))) +(push) +(check-sat) |