Match new z3 output

Data/SBV/Set.hs

@@ -145,8 +145,8 @@ complement ss
 --
 -- >>> prove $ \x (s :: SSet Integer) -> x `delete` (x `insert` s) .== s
 -- Falsifiable. Counter-example:
---   s0 =   2 :: Integer
---   s1 = {2} :: {Integer}
+--   s0 = 2 :: Integer
+--   s1 = U :: {Integer}
 --
 -- But the above is true if the element isn't in the set to start with:
 --
@@ -188,8 +188,8 @@ insert se ss
 --
 -- >>> prove $ \x (s :: SSet Integer) -> x `insert` (x `delete` s) .== s
 -- Falsifiable. Counter-example:
---   s0 =  2 :: Integer
---   s1 = {} :: {Integer}
+--   s0 =       2 :: Integer
+--   s1 = U - {2} :: {Integer}
 --
 -- But the above is true if the element is in the set to start with:
 --

Documentation/SBV/Examples/Misc/FirstOrderLogic.hs

@@ -137,8 +137,8 @@ Falsifiable. Counter-example:
   P _   = False
 <BLANKLINE>
   Q :: U -> Bool
-  Q U_2 = False
   Q U_0 = False
+  Q U_2 = False
   Q _   = True
 
 The solver found us a falsifying instance: Pick a domain with at least three elements. We'll call

Documentation/SBV/Examples/WeakestPreconditions/Sum.hs

@@ -237,18 +237,14 @@ The other way we can have a bad measure is if it fails to decrease through the l
 >>> let invariant SumS{n, i, s} = s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
 >>> let measure   SumS{n, i}    = [n + i]
 >>> void $ correctness invariant (Just measure)
-Following proof obligations failed:
-===================================
-  Measure for loop "i < n" is negative:
-    State  : SumS {n = 0, i = -1, s = 0}
-    Measure: -1
+Following proof obligation failed:
+==================================
   Measure for loop "i < n" does not decrease:
-    Before : SumS {n = 0, i = -1, s = 0}
-    Measure: -1
-    After  : SumS {n = 0, i = 0, s = 0}
-    Measure: 0
+    Before : SumS {n = 1, i = 0, s = 0}
+    Measure: 1
+    After  : SumS {n = 1, i = 1, s = 1}
+    Measure: 2
 
-Clearly, as @i@ increases, so does our bogus measure @n+i@. Note that in this case the counterexample has
-@i@ and @n@ as a negative value, as the SMT solver finds a counter-example to induction, not
-necessarily a reachable state. Obviously, all such failures need to be addressed for the full proof.
+Clearly, as @i@ increases, so does our bogus measure @n+i@. (Note that in this case the counterexample might have @i@ and @n@ as negative values, as the SMT solver finds a counter-example to induction, not
+necessarily a reachable state. Obviously, all such failures need to be addressed for the full proof.)
 -}

SBVTestSuite/GoldFiles/query1.gold

@@ -74,7 +74,7 @@
 [SEND] (get-info :reason-unknown)
 [RECV] (:reason-unknown "state of the most recent check-sat command is not known")
 [SEND] (get-info :version)
-[RECV] (:version "4.13.1")
+[RECV] (:version "4.13.4")
 [SEND] (get-info :status)
 [RECV] (:status sat)
 [GOOD] (define-fun s16 () Int 4)
@@ -105,7 +105,7 @@
 [SEND] (get-info :reason-unknown)
 [RECV] (:reason-unknown "unknown")
 [SEND] (get-info :version)
-[RECV] (:version "4.13.1")
+[RECV] (:version "4.13.4")
 [SEND] (get-info :memory)
 [RECV] unsupported
 [SEND] (get-info :time)
@@ -148,19 +148,19 @@
 [SEND] (get-proof)
 [RECV] ((set-logic ALL)
        (proof
-       (let (($x268 (<= s0 6)))
-       (let (($x269 (not $x268)))
-       (let (($x276 (or (not bey) $x269)))
-       (let ((@x274 (monotonicity (rewrite (= (> s0 6) $x269)) (= (=> bey (> s0 6)) (=> bey $x269)))))
-       (let ((@x280 (trans @x274 (rewrite (= (=> bey $x269) $x276)) (= (=> bey (> s0 6)) $x276))))
-       (let ((@x281 (mp (asserted (=> bey (> s0 6))) @x280 $x276)))
-       (let (($x293 (>= s0 6)))
-       (let (($x292 (not $x293)))
-       (let (($x300 (or (not hey) $x292)))
-       (let ((@x291 (trans (rewrite (= (< s0 6) (not (<= 6 s0)))) (rewrite (= (not (<= 6 s0)) $x292)) (= (< s0 6) $x292))))
-       (let ((@x304 (trans (monotonicity @x291 (= (=> hey (< s0 6)) (=> hey $x292))) (rewrite (= (=> hey $x292) $x300)) (= (=> hey (< s0 6)) $x300))))
-       (let ((@x305 (mp (asserted (=> hey (< s0 6))) @x304 $x300)))
-       (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x293 $x268)) (unit-resolution @x305 (asserted hey) $x292) (unit-resolution @x281 (asserted bey) $x269) false)))))))))))))))
+       (let (($x267 (<= s0 6)))
+       (let (($x268 (not $x267)))
+       (let (($x275 (or (not bey) $x268)))
+       (let ((@x273 (monotonicity (rewrite (= (> s0 6) $x268)) (= (=> bey (> s0 6)) (=> bey $x268)))))
+       (let ((@x279 (trans @x273 (rewrite (= (=> bey $x268) $x275)) (= (=> bey (> s0 6)) $x275))))
+       (let ((@x280 (mp (asserted (=> bey (> s0 6))) @x279 $x275)))
+       (let (($x292 (>= s0 6)))
+       (let (($x291 (not $x292)))
+       (let (($x299 (or (not hey) $x291)))
+       (let ((@x290 (trans (rewrite (= (< s0 6) (not (<= 6 s0)))) (rewrite (= (not (<= 6 s0)) $x291)) (= (< s0 6) $x291))))
+       (let ((@x303 (trans (monotonicity @x290 (= (=> hey (< s0 6)) (=> hey $x291))) (rewrite (= (=> hey $x291) $x299)) (= (=> hey (< s0 6)) $x299))))
+       (let ((@x304 (mp (asserted (=> hey (< s0 6))) @x303 $x299)))
+       (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x292 $x267)) (unit-resolution @x304 (asserted hey) $x291) (unit-resolution @x280 (asserted bey) $x268) false)))))))))))))))
 [SEND, TimeOut: 90000ms] (get-assertions)
 
 [RECV] ((! s7 :named |a > 0|)

SBVTestSuite/GoldFiles/set_tupleSet.gold

@@ -31,11 +31,12 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (mkSBVTuple2 (lambda ((x!1 Bool)) x!1) ((as const (Array Bool Bool)) true))))
+[RECV] ((s0 (mkSBVTuple2 (lambda ((x!1 Bool)) x!1)
+                    (store ((as const (Array Bool Bool)) false) false true))))
 *** Solver   : Z3
 *** Exit code: ExitSuccess
 
 FINAL:
 Satisfiable. Model:
-  s0 = ({True},U) :: ({Bool}, {Bool})
+  s0 = ({True},{False}) :: ({Bool}, {Bool})
 DONE!

SBVTestSuite/GoldFiles/set_uninterp1.gold

@@ -49,54 +49,54 @@ Fast allSat, Looking for solution 3
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (store ((as const (Array E Bool)) true) A false)))
+[RECV] ((s0 (store ((as const (Array E Bool)) false) B true)))
 [GOOD] (push 1)
-[GOOD] (define-fun s5 () (Array E Bool) (store ((as const (Array E Bool)) true) A false))
+[GOOD] (define-fun s5 () (Array E Bool) (store ((as const (Array E Bool)) false) B true))
 [GOOD] (define-fun s6 () Bool (distinct s0 s5))
 [GOOD] (assert s6)
 Fast allSat, Looking for solution 4
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (store (store ((as const (Array E Bool)) true) C false) A false)))
+[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) B true)))
 [GOOD] (push 1)
-[GOOD] (define-fun s7 () (Array E Bool) (store (store ((as const (Array E Bool)) true) C false) A false))
+[GOOD] (define-fun s7 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) B true))
 [GOOD] (define-fun s8 () Bool (distinct s0 s7))
 [GOOD] (assert s8)
 Fast allSat, Looking for solution 5
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (store (store ((as const (Array E Bool)) false) B true) A true)))
+[RECV] ((s0 ((as const (Array E Bool)) true)))
 [GOOD] (push 1)
-[GOOD] (define-fun s9 () (Array E Bool) (store (store ((as const (Array E Bool)) false) B true) A true))
+[GOOD] (define-fun s9 () (Array E Bool) ((as const (Array E Bool)) true))
 [GOOD] (define-fun s10 () Bool (distinct s0 s9))
 [GOOD] (assert s10)
 Fast allSat, Looking for solution 6
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) A true)))
+[RECV] ((s0 (store (store ((as const (Array E Bool)) false) B true) A true)))
 [GOOD] (push 1)
-[GOOD] (define-fun s11 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) A true))
+[GOOD] (define-fun s11 () (Array E Bool) (store (store ((as const (Array E Bool)) false) B true) A true))
 [GOOD] (define-fun s12 () Bool (distinct s0 s11))
 [GOOD] (assert s12)
 Fast allSat, Looking for solution 7
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (store (store ((as const (Array E Bool)) true) B false) A false)))
+[RECV] ((s0 (store ((as const (Array E Bool)) true) B false)))
 [GOOD] (push 1)
-[GOOD] (define-fun s13 () (Array E Bool) (store (store ((as const (Array E Bool)) true) B false) A false))
+[GOOD] (define-fun s13 () (Array E Bool) (store ((as const (Array E Bool)) true) B false))
 [GOOD] (define-fun s14 () Bool (distinct s0 s13))
 [GOOD] (assert s14)
 Fast allSat, Looking for solution 8
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (store (store (store ((as const (Array E Bool)) false) C true) B true) A true)))
+[RECV] ((s0 (store (store ((as const (Array E Bool)) true) B false) A false)))
 [GOOD] (push 1)
-[GOOD] (define-fun s15 () (Array E Bool) (store (store (store ((as const (Array E Bool)) false) C true) B true) A true))
+[GOOD] (define-fun s15 () (Array E Bool) (store (store ((as const (Array E Bool)) true) B false) A false))
 [GOOD] (define-fun s16 () Bool (distinct s0 s15))
 [GOOD] (assert s16)
 Fast allSat, Looking for solution 9
@@ -115,17 +115,17 @@ Fast allSat, Looking for solution 9
 
 FINAL:
 Solution #1:
-  s0 = {A,B,C} :: {E}
-Solution #2:
   s0 = U - {A,B} :: {E}
+Solution #2:
+  s0 = U - {B} :: {E}
 Solution #3:
-  s0 = {A,C} :: {E}
-Solution #4:
   s0 = {A,B} :: {E}
+Solution #4:
+  s0 = U :: {E}
 Solution #5:
-  s0 = U - {A,C} :: {E}
+  s0 = {B,C} :: {E}
 Solution #6:
-  s0 = U - {A} :: {E}
+  s0 = {B} :: {E}
 Solution #7:
   s0 = {A} :: {E}
 Solution #8: