From cdcdd49a79ba03966cbb29c4f380f426c95a7d3a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 10 Mar 2021 10:06:27 -0600 Subject: 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. --- test/regress/regress1/strings/issue6071-arith-prereg-i.smt2 | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 test/regress/regress1/strings/issue6071-arith-prereg-i.smt2 (limited to 'test') 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) -- cgit v1.2.3