Fix stale op list in sets (#2572)

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 317080ba6d8bb07350595b6ee773120c82baefbf..ec6406a6a2020697d8f259a6ffdc8a49b13c90e5 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -2247,7 +2247,7 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou
 }
   
 void TheorySetsPrivate::presolve() {
-
+  d_op_list.clear();
 }
 
 /**************************** eq::NotifyClass *****************************/

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index bec5362e5a8ae29b571dd7a8f151c049d9bdd147..0c68b1920c79772a844ae89a19dd675a29fd6090 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1466,6 +1466,7 @@ set(regress_1_tests
   regress1/sets/fuzz15201.smt2
   regress1/sets/fuzz31811.smt2
   regress1/sets/insert_invariant_37_2.smt2
+  regress1/sets/issue2568.smt2
   regress1/sets/lemmabug-ListElts317minimized.smt2
   regress1/sets/remove_check_free_31_6.smt2
   regress1/sets/sets-disequal.smt2

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 37c911d415a258497a038e6f47fe2e426765443b..4e77694b7e78b3a03f80dcccc6aab14930cfd46b 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1463,6 +1463,7 @@ REG1_TESTS = \
        regress1/sets/fuzz15201.smt2 \
        regress1/sets/fuzz31811.smt2 \
        regress1/sets/insert_invariant_37_2.smt2 \
+       regress1/sets/issue2568.smt2 \
        regress1/sets/lemmabug-ListElts317minimized.smt2 \
        regress1/sets/remove_check_free_31_6.smt2 \
        regress1/sets/sets-disequal.smt2 \

diff --git a/test/regress/regress1/sets/issue2568.smt2 b/test/regress/regress1/sets/issue2568.smt2
new file mode 100644 (file)
index 0000000..bb76e73
--- /dev/null
+++ b/test/regress/regress1/sets/issue2568.smt2
@@ -0,0 +1,21 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+
+(declare-datatypes () ((Unit (uu))))
+
+(declare-fun y () Int)
+(declare-fun b () Bool)
+(declare-fun s () (Set Int))
+(declare-fun u () Unit)
+
+(assert (= s (insert y s)))
+(assert (=> b (= uu u)))
+
+(push 1)
+(check-sat)
+(pop 1)
+
+(push 1)
+(check-sat)