(proof-new) Miscellaneous fixes and regressions (#5841)

4 files changed, 106 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4cee236c1..b9fb10267 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -709,6 +709,7 @@ set(regress_0_tests
   regress0/nl/sqrt.smt2
   regress0/nl/sqrt2-value.smt2
   regress0/nl/subs0-unsat-confirm.smt2
+  regress0/nl/tpp-fail-pf-012921.smt2
   regress0/nl/very-easy-sat.smt2
   regress0/nl/very-simple-unsat.smt2
   regress0/opt-abd-no-use.smt2
@@ -749,6 +750,7 @@ set(regress_0_tests
   regress0/precedence/xor-and.cvc
   regress0/precedence/xor-assoc.cvc
   regress0/precedence/xor-or.cvc
+  regress0/preprocess/circuit-prop.smt2
   regress0/preprocess/preprocess_00.cvc
   regress0/preprocess/preprocess_01.cvc
   regress0/preprocess/preprocess_02.cvc
@@ -1457,6 +1459,7 @@ set(regress_1_tests
   regress1/bv/incorrect1.smtv1.smt2
   regress1/bv/issue3654.smt2
   regress1/bv/issue3776.smt2
+  regress1/bv/min-pp-rewrite-error.smt2
   regress1/bv/test-bv-abstraction.smt2
   regress1/bv/unsound1.smt2
   regress1/bvdiv2.smt2
diff --git a/test/regress/regress0/nl/tpp-fail-pf-012921.smt2 b/test/regress/regress0/nl/tpp-fail-pf-012921.smt2
new file mode 100644
index 000000000..c97a12074
--- /dev/null
+++ b/test/regress/regress0/nl/tpp-fail-pf-012921.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () Real)
+(assert (and (> 0.0 x) (not (= 0.0 (/ 0.0 (* 2 x))))))
+(check-sat)
diff --git a/test/regress/regress0/preprocess/circuit-prop.smt2 b/test/regress/regress0/preprocess/circuit-prop.smt2
new file mode 100644
index 000000000..69271636d
--- /dev/null
+++ b/test/regress/regress0/preprocess/circuit-prop.smt2
@@ -0,0 +1,94 @@
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: unsat
+
+;;;;; iteEvalThen(true)
+(set-logic ALL)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(assert a)
+(assert b)
+(assert (not (ite a b c)))
+(check-sat)
+
+(reset)
+
+;;;;; iteEvalThen(false)
+(set-logic ALL)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(assert a)
+(assert (not b))
+(assert (or (ite a b c) d))
+(check-sat)
+
+(reset)
+
+;;;;; iteEvalElse(true)
+(set-logic ALL)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(assert (not a))
+(assert c)
+(assert (not (ite a b c)))
+(check-sat)
+
+(reset)
+
+;;;;; iteEvalElse(false)
+(set-logic ALL)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(assert (not a))
+(assert (not c))
+(assert (or (ite a b c) d))
+(check-sat)
+
+(reset)
+
+(set-logic ALL)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(assert a)
+(assert b)
+(assert (=> a c))
+(assert (=> b (not c)))
+(check-sat)
+
+(reset)
+
+(set-logic ALL)
+(assert false)
+(check-sat)
+
+(reset)
+
+(set-logic ALL)
+(declare-fun x () Bool)
+(declare-fun z () Bool)
+(assert (= x z))
+(assert (not x))
+(assert z)
+(check-sat)
+
+(reset)
+
+(set-logic ALL)
+(declare-fun x3 () Bool)
+(declare-fun x9 () Bool)
+(assert (not x3))
+(assert (or x3 (and x9 x3)))
+(check-sat)
diff --git a/test/regress/regress1/bv/min-pp-rewrite-error.smt2 b/test/regress/regress1/bv/min-pp-rewrite-error.smt2
new file mode 100644
index 000000000..510612762
--- /dev/null
+++ b/test/regress/regress1/bv/min-pp-rewrite-error.smt2
@@ -0,0 +1,4 @@
+(set-logic QF_BV)
+(set-info :status unsat)
+(declare-fun v2 () (_ BitVec 4))
+(check-sat-assuming ((and (not (= (_ bv1 4) ((_ sign_extend 3) (ite (bvsgt v2 (_ bv0 4)) (_ bv1 1) (_ bv0 1))))) (bvsge (_ bv1 1) (bvnand (_ bv1 1) (ite (= (_ bv1 4) ((_ sign_extend 3) (ite (bvslt v2 (_ bv0 4)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))) (bvsgt (_ bv0 4) ((_ sign_extend 3) (ite (bvsle (_ bv0 1) (ite (bvsle (_ bv1 1) (ite (bvugt (_ bv1 4) ((_ sign_extend 3) (ite (bvuge v2 (_ bv1 4)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))))))