From: Kshitij Bansal Date: Wed, 11 Jun 2014 16:33:17 +0000 (-0400) Subject: user/sat context issue in sets X-Git-Tag: cvc5-1.0.0~6837^2~3 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=455123f08cb9001bfa05f94030db8e1d776381c7;p=cvc5.git user/sat context issue in sets --- diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 9b628ede2..3ca446ec5 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -831,8 +831,8 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_propagationQueue(c), d_settermPropagationQueue(c), d_nodeSaver(c), - d_pending(u), - d_pendingDisequal(u), + d_pending(c), + d_pendingDisequal(c), d_pendingEverInserted(u), d_scrutinize(NULL) { diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 8516dbc0c..7b8a06038 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -46,6 +46,7 @@ TESTS = \ error2.smt2 \ eqtest.smt2 \ fuzz15201.smt2 \ + fuzz14418.smt2 \ rec_copy_loop_check_heap_access_43_4.smt2 \ sets-disequal.smt2 \ sets-equal.smt2 \ diff --git a/test/regress/regress0/sets/fuzz14418.smt2 b/test/regress/regress0/sets/fuzz14418.smt2 new file mode 100644 index 000000000..d5a49c601 --- /dev/null +++ b/test/regress/regress0/sets/fuzz14418.smt2 @@ -0,0 +1,171 @@ +; symptom: assertion failure in EqEngine : hasTerm(t) +; +; issue: had some nodes in d_pending, even though sat context had been popped, +; and those were no longer relevant. +; +; fix: make pending queues sat context depending. d_pendingEverInserted which +; is still user-context dependent takes care of not generating a lemma twice. +; +; sat +(set-info :source |fuzzsmt|) +(set-info :smt-lib-version 2.0) +(set-info :category "random") +(set-info :status sat) +(set-logic QF_UFLIA_SETS) +(define-sort Element () Int) +(declare-fun f0 ( Int) Int) +(declare-fun f1 ( (Set Element) (Set Element) (Set Element)) (Set Element)) +(declare-fun p0 ( Int Int) Bool) +(declare-fun p1 ( (Set Element)) Bool) +(declare-fun v0 () Int) +(declare-fun v1 () (Set Element)) +(declare-fun v2 () (Set Element)) +(declare-fun v3 () (Set Element)) +(declare-fun v4 () (Set Element)) +(assert (let ((e5 7)) +(let ((e6 (* e5 v0))) +(let ((e7 (* v0 e5))) +(let ((e8 (f0 e6))) +(let ((e9 (* v0 (- e5)))) +(let ((e10 (f0 v0))) +(let ((e11 (* (- e5) e10))) +(let ((e12 (ite (p0 e7 e6) 1 0))) +(let ((e13 (union v3 v4))) +(let ((e14 (setminus v2 v2))) +(let ((e15 (f1 v1 v4 v1))) +(let ((e16 (f1 e14 v1 v4))) +(let ((e17 (intersection e16 e15))) +(let ((e18 (f1 v4 e15 v2))) +(let ((e19 (ite (p1 e13) (setenum 1) (setenum 0)))) +(let ((e20 (in v0 e17))) +(let ((e21 (in e7 e16))) +(let ((e22 (in e10 e16))) +(let ((e23 (in e8 e17))) +(let ((e24 (in e9 e14))) +(let ((e25 (in e8 e16))) +(let ((e26 (in v0 e13))) +(let ((e27 (in e12 v4))) +(let ((e28 (in e8 e14))) +(let ((e29 (in e8 v1))) +(let ((e30 (in e10 e13))) +(let ((e31 (in e7 e13))) +(let ((e32 (f1 e13 e13 e13))) +(let ((e33 (f1 e18 v4 e17))) +(let ((e34 (f1 v2 v2 e15))) +(let ((e35 (f1 e33 e18 e15))) +(let ((e36 (f1 e19 e14 e17))) +(let ((e37 (f1 e34 e18 e34))) +(let ((e38 (f1 v3 e34 e18))) +(let ((e39 (f1 e16 v4 e13))) +(let ((e40 (f1 v1 e34 e15))) +(let ((e41 (< e10 e11))) +(let ((e42 (= e6 e12))) +(let ((e43 (> e6 e11))) +(let ((e44 (< e12 e8))) +(let ((e45 (< e7 e10))) +(let ((e46 (= e11 e12))) +(let ((e47 (= e11 e7))) +(let ((e48 (<= e11 e10))) +(let ((e49 (p0 e9 e9))) +(let ((e50 (>= v0 e10))) +(let ((e51 (ite e22 e14 e33))) +(let ((e52 (ite e45 e16 e37))) +(let ((e53 (ite e42 e39 e17))) +(let ((e54 (ite e21 e39 e33))) +(let ((e55 (ite e29 e13 e13))) +(let ((e56 (ite e48 e15 e34))) +(let ((e57 (ite e50 e38 e53))) +(let ((e58 (ite e47 e32 v1))) +(let ((e59 (ite e20 e36 e33))) +(let ((e60 (ite e28 e35 v2))) +(let ((e61 (ite e48 e40 e38))) +(let ((e62 (ite e30 e38 e53))) +(let ((e63 (ite e22 v4 e19))) +(let ((e64 (ite e46 e60 e53))) +(let ((e65 (ite e25 e61 e16))) +(let ((e66 (ite e23 v3 e38))) +(let ((e67 (ite e49 v4 e18))) +(let ((e68 (ite e21 e54 v3))) +(let ((e69 (ite e25 e15 v4))) +(let ((e70 (ite e20 e55 e19))) +(let ((e71 (ite e27 e38 e36))) +(let ((e72 (ite e28 e14 e33))) +(let ((e73 (ite e42 e66 e60))) +(let ((e74 (ite e26 e54 e69))) +(let ((e75 (ite e28 e68 e71))) +(let ((e76 (ite e24 e33 e52))) +(let ((e77 (ite e44 e40 e74))) +(let ((e78 (ite e48 e32 e51))) +(let ((e79 (ite e22 e34 e62))) +(let ((e80 (ite e22 e78 e73))) +(let ((e81 (ite e22 e13 e55))) +(let ((e82 (ite e43 e37 e70))) +(let ((e83 (ite e48 e59 e80))) +(let ((e84 (ite e29 e15 e77))) +(let ((e85 (ite e41 e19 e35))) +(let ((e86 (ite e22 e63 e69))) +(let ((e87 (ite e26 e19 e70))) +(let ((e88 (ite e46 e37 e53))) +(let ((e89 (ite e25 e70 e76))) +(let ((e90 (ite e31 v4 e73))) +(let ((e91 (ite e46 e12 e8))) +(let ((e92 (ite e43 e11 e6))) +(let ((e93 (ite e50 e10 e7))) +(let ((e94 (ite e21 e8 e7))) +(let ((e95 (ite e27 v0 e6))) +(let ((e96 (ite e24 e9 e92))) +(let ((e97 (ite e22 e6 e92))) +(let ((e98 (ite e49 e96 e12))) +(let ((e99 (ite e27 e98 e6))) +(let ((e100 (ite e31 e11 e8))) +(let ((e101 (ite e26 e12 v0))) +(let ((e102 (ite e22 e92 e96))) +(let ((e103 (ite e28 e92 e6))) +(let ((e104 (ite e27 e12 v0))) +(let ((e105 (ite e23 e101 e9))) +(let ((e106 (ite e47 e11 e104))) +(let ((e107 (ite e45 e105 e100))) +(let ((e108 (ite e48 e12 e9))) +(let ((e109 (ite e42 e96 e91))) +(let ((e110 (ite e29 e11 e101))) +(let ((e111 (ite e50 e107 e110))) +(let ((e112 (ite e29 e104 e92))) +(let ((e113 (ite e20 e108 e12))) +(let ((e114 (ite e44 e96 e104))) +(let ((e115 (ite e41 e105 e110))) +(let ((e116 (ite e41 e6 e103))) +(let ((e117 (ite e28 e92 e114))) +(let ((e118 (ite e30 e111 e113))) +(let ((e119 (ite e30 e109 e8))) +(let ((e120 (ite e25 e12 e118))) +(let ((e121 (xor e46 e42))) +(let ((e122 (xor e28 e29))) +(let ((e123 (= e122 e49))) +(let ((e124 (and e43 e45))) +(let ((e125 (or e121 e23))) +(let ((e126 (and e125 e24))) +(let ((e127 (= e41 e126))) +(let ((e128 (xor e124 e44))) +(let ((e129 (not e26))) +(let ((e130 (= e22 e123))) +(let ((e131 (not e20))) +(let ((e132 (and e127 e27))) +(let ((e133 (=> e50 e131))) +(let ((e134 (=> e132 e30))) +(let ((e135 (xor e128 e48))) +(let ((e136 (ite e129 e47 e129))) +(let ((e137 (and e133 e130))) +(let ((e138 (or e136 e134))) +(let ((e139 (and e31 e31))) +(let ((e140 (not e137))) +(let ((e141 (= e140 e139))) +(let ((e142 (= e25 e21))) +(let ((e143 (not e142))) +(let ((e144 (and e143 e135))) +(let ((e145 (and e144 e138))) +(let ((e146 (and e145 e145))) +(let ((e147 (= e141 e146))) +e147 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + +(check-sat)