Revert "Revert "match new z3 output""

This reverts commit e8d2d42.
LeventErkok · Nov 20, 2023 · 8f7aaca · 8f7aaca
1 parent ea13d8b
commit 8f7aaca
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 17 deletions.
diff --git a/SBVTestSuite/GoldFiles/set_tupleSet.gold b/SBVTestSuite/GoldFiles/set_tupleSet.gold
@@ -34,11 +34,11 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (mkSBVTuple2 ((as const (Array Bool Bool)) true) (lambda ((x!1 Bool)) x!1))))
+[RECV] ((s0 (mkSBVTuple2 (lambda ((x!1 Bool)) x!1) ((as const (Array Bool Bool)) true))))
 *** Solver   : Z3
 *** Exit code: ExitSuccess
 
 FINAL:
 Satisfiable. Model:
-  s0 = (U,{True}) :: ({Bool}, {Bool})
+  s0 = ({True},U) :: ({Bool}, {Bool})
 DONE!
diff --git a/SBVTestSuite/GoldFiles/set_uninterp1.gold b/SBVTestSuite/GoldFiles/set_uninterp1.gold
@@ -64,49 +64,49 @@ Fast allSat, Looking for solution 4
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (store ((as const (Array E Bool)) false) C true)))
+[RECV] ((s0 (store ((as const (Array E Bool)) true) A false)))
 [GOOD] (push 1)
-[GOOD] (define-fun s10 () (Array E Bool) (store ((as const (Array E Bool)) false) C true))
+[GOOD] (define-fun s10 () (Array E Bool) (store ((as const (Array E Bool)) true) A false))
 [GOOD] (define-fun s11 () Bool (= s0 s10))
 [GOOD] (define-fun s12 () Bool (not s11))
 [GOOD] (assert s12)
 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) C true) A true)))
+[RECV] ((s0 (store ((as const (Array E Bool)) false) C true)))
 [GOOD] (push 1)
-[GOOD] (define-fun s13 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) A true))
+[GOOD] (define-fun s13 () (Array E Bool) (store ((as const (Array E Bool)) false) C true))
 [GOOD] (define-fun s14 () Bool (= s0 s13))
 [GOOD] (define-fun s15 () Bool (not s14))
 [GOOD] (assert s15)
 Fast allSat, Looking for solution 6
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 ((as const (Array E Bool)) true)))
+[RECV] ((s0 (store (store ((as const (Array E Bool)) false) B true) A true)))
 [GOOD] (push 1)
-[GOOD] (define-fun s16 () (Array E Bool) ((as const (Array E Bool)) true))
+[GOOD] (define-fun s16 () (Array E Bool) (store (store ((as const (Array E Bool)) false) B true) A true))
 [GOOD] (define-fun s17 () Bool (= s0 s16))
 [GOOD] (define-fun s18 () Bool (not s17))
 [GOOD] (assert s18)
 Fast allSat, Looking for solution 7
 [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 (store (store ((as const (Array E Bool)) false) C true) A true)))
 [GOOD] (push 1)
-[GOOD] (define-fun s19 () (Array E Bool) (store (store ((as const (Array E Bool)) false) B true) A true))
+[GOOD] (define-fun s19 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) A true))
 [GOOD] (define-fun s20 () Bool (= s0 s19))
 [GOOD] (define-fun s21 () Bool (not s20))
 [GOOD] (assert s21)
 Fast allSat, Looking for solution 8
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) B true)))
+[RECV] ((s0 ((as const (Array E Bool)) true)))
 [GOOD] (push 1)
-[GOOD] (define-fun s22 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) B true))
+[GOOD] (define-fun s22 () (Array E Bool) ((as const (Array E Bool)) true))
 [GOOD] (define-fun s23 () Bool (= s0 s22))
 [GOOD] (define-fun s24 () Bool (not s23))
 [GOOD] (assert s24)
@@ -126,15 +126,15 @@ Fast allSat, Looking for solution 9
 
 FINAL:
 Solution #1:
-  s0 = {B,C} :: {E}
+  s0 = U :: {E}
 Solution #2:
-  s0 = {A,B} :: {E}
+  s0 = {A,C} :: {E}
 Solution #3:
-  s0 = U :: {E}
+  s0 = {A,B} :: {E}
 Solution #4:
-  s0 = {A,C} :: {E}
-Solution #5:
   s0 = {C} :: {E}
+Solution #5:
+  s0 = U - {A} :: {E}
 Solution #6:
   s0 = {B} :: {E}
 Solution #7: