diff options
Diffstat (limited to 'test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2')
| -rw-r--r-- | test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 index 5fa5101f0..df659f0fb 100644 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 @@ -8,12 +8,12 @@ ; What was going on? ; ; The solver was unable to reason that (emptyset) cannot equal -; (setenum 0). There were no membership predicates anywhere, just +; (singleton 0). There were no membership predicates anywhere, just ; equalities. ; ; Fix ; -; Add the propagation rule: (true) => (in x (setenum x)) +; Add the propagation rule: (true) => (member x (singleton x)) (declare-fun z3f70 (Int) (Set Int)) (declare-fun z3v85 () Int) @@ -21,7 +21,7 @@ (declare-fun z3v87 () Int) (declare-fun z3v90 () Int) -(assert (= (z3f70 z3v90) (union (z3f70 z3v85) (union (as emptyset (Set Int)) (setenum z3v86))))) +(assert (= (z3f70 z3v90) (union (z3f70 z3v85) (union (as emptyset (Set Int)) (singleton z3v86))))) (assert (= (z3f70 z3v90) (z3f70 z3v87))) (assert (= (as emptyset (Set Int)) (z3f70 z3v87))) (check-sat) |