From e9f4cec2cad02e270747759223090c16b9d2d44c Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 10 Mar 2020 14:51:32 -0700
Subject: Fix issue with reset-assertions. (#3988)

Calling (reset-assertions) in start mode was not handled correctly.
Additionally, when calling (check-sat) after (reset-assertions) after a
(check-sat) call that answered unsat, we answered unsat instead of sat.
This cleans up and fixes reset-assertions) handling.
---
 test/regress/CMakeLists.txt                            |  4 +++-
 test/regress/regress0/reset-assertions.smt2            | 17 -----------------
 .../regress0/smtlib/reset-assertions-global.smt2       | 18 ++++++++++++++++++
 test/regress/regress0/smtlib/reset-assertions1.smt2    | 11 +++++++++++
 test/regress/regress0/smtlib/reset-assertions2.smt2    | 17 +++++++++++++++++
 5 files changed, 49 insertions(+), 18 deletions(-)
 delete mode 100644 test/regress/regress0/reset-assertions.smt2
 create mode 100644 test/regress/regress0/smtlib/reset-assertions-global.smt2
 create mode 100644 test/regress/regress0/smtlib/reset-assertions1.smt2
 create mode 100644 test/regress/regress0/smtlib/reset-assertions2.smt2

(limited to 'test/regress')

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6579894e9..a9017ac20 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -816,7 +816,6 @@ set(regress_0_tests
   regress0/rels/rel_transpose_7.cvc
   regress0/rels/relations-ops.smt2
   regress0/rels/rels-sharing-simp.cvc
-  regress0/reset-assertions.smt2
   regress0/sep/dispose-1.smt2
   regress0/sep/dup-nemp.smt2
   regress0/sep/issue3720-check-model.smt2
@@ -897,6 +896,9 @@ set(regress_0_tests
   regress0/smtlib/get-unsat-assumptions.smt2
   regress0/smtlib/global-decls.smt2
   regress0/smtlib/reason-unknown.smt2
+  regress0/smtlib/reset-assertions1.smt2
+  regress0/smtlib/reset-assertions2.smt2
+  regress0/smtlib/reset-assertions-global.smt2
   regress0/smtlib/reset-force-logic.smt2
   regress0/smtlib/reset-set-logic.smt2
   regress0/smtlib/set-info-status.smt2
diff --git a/test/regress/regress0/reset-assertions.smt2 b/test/regress/regress0/reset-assertions.smt2
deleted file mode 100644
index 3c37f2cba..000000000
--- a/test/regress/regress0/reset-assertions.smt2
+++ /dev/null
@@ -1,17 +0,0 @@
-; EXPECT: sat
-; EXPECT: sat
-(set-logic QF_ALL)
-(set-option :incremental true)
-(set-option :produce-models true)
-
-(declare-fun x () Real)
-(declare-fun y () Real)
-(assert (> x 0.0))
-(assert (> y 0.0))
-(assert (= (+ (* 2 x) y) 4))
-(check-sat)
-(reset-assertions)
-
-(declare-fun a () (Array Int Int))
-(assert (= (select a 4) 10))
-(check-sat)
diff --git a/test/regress/regress0/smtlib/reset-assertions-global.smt2 b/test/regress/regress0/smtlib/reset-assertions-global.smt2
new file mode 100644
index 000000000..f6e2aaed2
--- /dev/null
+++ b/test/regress/regress0/smtlib/reset-assertions-global.smt2
@@ -0,0 +1,18 @@
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: unsat
+(set-option :global-declarations true)
+(set-logic QF_BV)
+(set-option :incremental true)
+(declare-fun x2 () (_ BitVec 3))
+(declare-fun x1 () (_ BitVec 3))
+(declare-fun x0 () (_ BitVec 3))
+(assert (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1))
+(assert (= #b000 x2))
+(check-sat)
+(reset-assertions)
+(assert (= x2 x1))
+(check-sat)
+(reset-assertions)
+(assert (distinct x1 x1))
+(check-sat)
diff --git a/test/regress/regress0/smtlib/reset-assertions1.smt2 b/test/regress/regress0/smtlib/reset-assertions1.smt2
new file mode 100644
index 000000000..7b4006c5d
--- /dev/null
+++ b/test/regress/regress0/smtlib/reset-assertions1.smt2
@@ -0,0 +1,11 @@
+; EXPECT: unsat
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun v0 () (_ BitVec 4))
+(set-option :produce-models true)
+(reset-assertions)
+(set-option :incremental true)
+(assert (and (= v0 (_ bv0 4)) (distinct v0 (_ bv0 4))))
+(check-sat)
+(reset-assertions)
+(check-sat)
diff --git a/test/regress/regress0/smtlib/reset-assertions2.smt2 b/test/regress/regress0/smtlib/reset-assertions2.smt2
new file mode 100644
index 000000000..3c37f2cba
--- /dev/null
+++ b/test/regress/regress0/smtlib/reset-assertions2.smt2
@@ -0,0 +1,17 @@
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_ALL)
+(set-option :incremental true)
+(set-option :produce-models true)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+(assert (> x 0.0))
+(assert (> y 0.0))
+(assert (= (+ (* 2 x) y) 4))
+(check-sat)
+(reset-assertions)
+
+(declare-fun a () (Array Int Int))
+(assert (= (select a 4) 10))
+(check-sat)
-- 
cgit v1.2.3