Integrate central equality engine approach into theory engine, add option and regressions (#6943)

This commit makes TheoryEngine take into account whether theories are using the central equality engine. 

With this commit, the central equality engine can now be optionally enabled via `--ee-mode=central`.

12 files changed, 202 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 151e01088..902037088 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -120,6 +120,7 @@ set(regress_0_tests
   regress0/aufbv/bug493.smtv1.smt2
   regress0/aufbv/bug509.smtv1.smt2
   regress0/aufbv/bug580.delta.smt2
+  regress0/aufbv/cee-small-shared-eq.smt2
   regress0/aufbv/diseqprop.01.smtv1.smt2
   regress0/aufbv/dubreva005ue.delta01.smtv1.smt2
   regress0/aufbv/fifo32bc06k08.delta01.smtv1.smt2
@@ -468,6 +469,7 @@ set(regress_0_tests
   regress0/datatypes/bug597-rbt.smt2
   regress0/datatypes/bug604.smt2
   regress0/datatypes/bug625.smt2
+  regress0/datatypes/canExp-dtPendingMerge.smt2
   regress0/datatypes/cdt-model-cade15.smt2
   regress0/datatypes/cdt-non-canon-stream.smt2
   regress0/datatypes/coda_simp_model.smt2
@@ -1084,6 +1086,7 @@ set(regress_0_tests
   regress0/sets/pre-proc-univ.smt2
   regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
   regress0/sets/setel-eq.smt2
+  regress0/sets/sets-deq-dd.smt2
   regress0/sets/sets-equal.smt2
   regress0/sets/sets-extr.smt2
   regress0/sets/sets-inter.smt2
@@ -1542,10 +1545,12 @@ set(regress_1_tests
   regress1/bv/test-bv-abstraction.smt2
   regress1/bv/unsound1.smt2
   regress1/bvdiv2.smt2
+  regress1/cee-bug0909-dd-scope.smt2
   regress1/constarr3.cvc
   regress1/constarr3.smt2
   regress1/cores/issue5604.smt2
   regress1/datatypes/acyclicity-sr-ground096.smt2
+  regress1/datatypes/cee-prs-small-dd2.smt2
   regress1/datatypes/dt-color-2.6.smt2
   regress1/datatypes/dt-param-card4-unsat.smt2
   regress1/datatypes/error.cvc
@@ -1734,6 +1739,7 @@ set(regress_1_tests
   regress1/push-pop/arith_lra_02.smt2
   regress1/push-pop/bug-fmf-fun-skolem.smt2
   regress1/push-pop/bug216.smt2
+  regress1/push-pop/cee-prs-small.smt2
   regress1/push-pop/fuzz_1.smt2
   regress1/push-pop/fuzz_10.smt2
   regress1/push-pop/fuzz_11.smt2
@@ -1813,6 +1819,8 @@ set(regress_1_tests
   regress1/quantifiers/burns13.smt2
   regress1/quantifiers/burns4.smt2
   regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
+  regress1/quantifiers/cee-npnt-dd.smt2
+  regress1/quantifiers/cee-os-delta.smt2
   regress1/quantifiers/cdt-0208-to.smt2
   regress1/quantifiers/const.cvc
   regress1/quantifiers/constfunc.cvc
@@ -2088,6 +2096,7 @@ set(regress_1_tests
   regress1/strings/bug686dd.smt2
   regress1/strings/bug768.smt2
   regress1/strings/bug799-min.smt2
+  regress1/strings/cee-norn-aes-trivially.smt2 
   regress1/strings/chapman150408.smt2
   regress1/strings/cmu-2db2-extf-reg.smt2
   regress1/strings/cmu-5042-0707-2.smt2
@@ -2482,6 +2491,7 @@ set(regress_2_tests
   regress2/piVC_5581bd.smt2
   regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
   regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
+  regress2/quantifiers/cee-event-wrong-sat.smt2
   regress2/quantifiers/gn-wrong-091018.smt2
   regress2/quantifiers/issue3481-unsat1.smt2
   regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2
@@ -2722,6 +2732,7 @@ set(regression_disabled_tests
   # previously sygus inference did not apply, now (correctly) times out
   regress1/sygus/issue3498.smt2
   regress2/arith/miplib-opt1217--27.smt2
+  regress2/quantifiers/exp-trivially-dd3.smt2
   regress2/nl/dumortier-050317.smt2
   # timeout on some builds after changes to justification heuristic
   regress2/nl/nt-lemmas-bad.smt2
diff --git a/test/regress/regress0/aufbv/cee-small-shared-eq.smt2 b/test/regress/regress0/aufbv/cee-small-shared-eq.smt2
new file mode 100644
index 000000000..fa91fe7de
--- /dev/null
+++ b/test/regress/regress0/aufbv/cee-small-shared-eq.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Array (_ BitVec 1) (_ BitVec 16)))
+(assert (not (= (_ bv0 16) (select a ((_ extract 14 14) (select a (_ bv0 1)))))))
+(check-sat)
diff --git a/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2 b/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2
new file mode 100644
index 000000000..d81c3723d
--- /dev/null
+++ b/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((T 0)) (((A) (B (proj0B T) (proj1B T)) (C (proj0C T)) (D (proj0D T) ))))
+(declare-fun w () T)
+(declare-fun u () T)
+(assert (= w (B (D u) (B (D u) (C w)))))
+(check-sat)
diff --git a/test/regress/regress0/sets/sets-deq-dd.smt2 b/test/regress/regress0/sets/sets-deq-dd.smt2
new file mode 100644
index 000000000..17ca1fce2
--- /dev/null
+++ b/test/regress/regress0/sets/sets-deq-dd.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun S () (Set (_ BitVec 1)))
+(assert (not (= S (as emptyset (Set (_ BitVec 1))))))
+(check-sat)
diff --git a/test/regress/regress1/cee-bug0909-dd-scope.smt2 b/test/regress/regress1/cee-bug0909-dd-scope.smt2
new file mode 100644
index 000000000..6ce621a98
--- /dev/null
+++ b/test/regress/regress1/cee-bug0909-dd-scope.smt2
@@ -0,0 +1,23 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((x5 0)) (((x3) (x4))))
+(declare-sort x 0)
+(declare-sort x1 0)
+(declare-datatypes ((x22 0)) (((x2))))
+(declare-datatypes ((x2 0)) (((x2 (x2 x5) (x24 x5) (x25 Int) (x26 Int) (x27 Int)))))
+(declare-sort x30 0)
+(declare-sort x3 0)
+(declare-datatypes ((x4 0)) (((x44 (x43 x3)))))
+(declare-fun x46 (x3) x1)
+(declare-datatypes ((x54 0)) (((x49 (x48 x22)) (x5 (x5 x2)) (d (s x1)))))
+(declare-fun x5 (x22) x2)
+(declare-fun x67 () (Array x x54))
+(declare-fun x6 () (Array x x54))
+(declare-fun x7 () (Array x30 x4))
+(declare-fun x63 () x30)
+(declare-fun x () x)
+(assert (distinct x3 (ite (or (distinct x6 (store x67 x (d (x46 (x43 (select x7 x63)))))) (= x67 (store x67 x (x5 (x2 x4 x3 (x25 (x5 (x48 (select x67 x)))) (x26 (x5 (x48 (select x67 x)))) (x27 (x5 (x48 (select x6 x))))))))) x3 x4)))
+(check-sat)
diff --git a/test/regress/regress1/datatypes/cee-prs-small-dd2.smt2 b/test/regress/regress1/datatypes/cee-prs-small-dd2.smt2
new file mode 100644
index 000000000..fe422d9e4
--- /dev/null
+++ b/test/regress/regress1/datatypes/cee-prs-small-dd2.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((r 0)) (((R (x Int)))))
+(declare-datatype t ((M (t1 (Array Int Int)) (t2 (Array Int Int)))))
+(declare-datatypes ((q 0)) (((R (x (Array Int r)) (y t)))))
+(declare-fun z () q)
+(assert (= z (R ((as const (Array Int r)) (R 0)) (M ((as const (Array Int Int)) 1) ((as const (Array Int Int)) 0)))))
+(assert (= (x (select (x z) 0)) (select (t1 (y z)) 1)))
+(check-sat)
diff --git a/test/regress/regress1/push-pop/cee-prs-small.smt2 b/test/regress/regress1/push-pop/cee-prs-small.smt2
new file mode 100644
index 000000000..4c0b06764
--- /dev/null
+++ b/test/regress/regress1/push-pop/cee-prs-small.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: -i --ee-mode=distributed
+; COMMAND-LINE: -i --ee-mode=central
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic ALL)
+(declare-datatypes ((r 0)) (((r_ctor (x Int)))))
+(declare-datatype tup ((mkt (t1 (Array Int Int)) (t2 (Array Int Int)))))
+(declare-datatypes ((q 0)) (((R (x (Array Int r)) (y tup)))))
+(declare-fun z () q)
+(assert (not (= 1 (select (t2 (y z)) 1))))
+(assert (= z (R ((as const (Array Int r)) (r_ctor 0)) (mkt ((as const (Array Int Int)) 1) ((as const (Array Int Int)) 0)))))
+(check-sat)
+(assert (= (x (select (x z) 0)) (select (t1 (y z)) 1)))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/cee-npnt-dd.smt2 b/test/regress/regress1/quantifiers/cee-npnt-dd.smt2
new file mode 100644
index 000000000..15727589d
--- /dev/null
+++ b/test/regress/regress1/quantifiers/cee-npnt-dd.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(set-option :fmf-bound true)
+(declare-datatype N ((o) (f) (s)))
+(declare-datatype P ((P)))
+(declare-fun G (N P Int) Bool)
+(declare-datatype c ((c (_p P))))
+(declare-fun g (N Int Int) c)
+(assert (forall ((x N)) (not (G x P 0))))
+(assert (forall ((t Int)) (or (< t 0) (> t 1) (and (forall ((p P)) (or (exists ((y N)) (and (G y (_p (g y 0 0)) t)))))))))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/cee-os-delta.smt2 b/test/regress/regress1/quantifiers/cee-os-delta.smt2
new file mode 100644
index 000000000..803291aa3
--- /dev/null
+++ b/test/regress/regress1/quantifiers/cee-os-delta.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed
+; COMMAND-LINE: --full-saturate-quant --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun o (Int) Int)
+(declare-fun f (Int Int) Int)
+(assert (forall ((x Int)) (forall ((y Int)) (! (= 1 (* y (div y y))) :pattern ((f x y))))))
+(assert (= 0 (f (o 0) (o 1))))
+(check-sat)
diff --git a/test/regress/regress1/strings/cee-norn-aes-trivially.smt2 b/test/regress/regress1/strings/cee-norn-aes-trivially.smt2
new file mode 100644
index 000000000..2f8d9904d
--- /dev/null
+++ b/test/regress/regress1/strings/cee-norn-aes-trivially.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --arith-eq-solver --ee-mode=distributed
+; COMMAND-LINE: --arith-eq-solver --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun v () String)
+(assert (str.in_re (str.++ "" v) (re.* (str.to_re "z"))))
+(assert (str.in_re v (re.* (re.range "a" "u"))))
+(assert (not (str.in_re v (str.to_re ""))))
+(check-sat)
diff --git a/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2
new file mode 100644
index 000000000..c0b3aac7c
--- /dev/null
+++ b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2
@@ -0,0 +1,43 @@
+; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed
+; COMMAND-LINE: --full-saturate-quant --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((T@$TypeValue 0) (T@A 0)) (((A)) ((T))))
+(declare-datatypes ((T@$Location 0)) (((P) (G (|t# | T@$TypeValue) (|a#G| Int)))))
+(declare-sort |T@[Int]$Value| 0)
+(declare-datatypes ((T@$Value 0) (T@R 0)) (((E) ($Boolean (|b#$Boolean| Bool)) (I (|i#I| Int)) (D (|a#D| Int)) (V (|v#V| T@R))) ((R (|v#R| |T@[Int]$Value|) (|l#R| Int)))))
+(declare-sort b 0)
+(declare-sort l 0)
+(declare-datatypes ((T@M 0)) (((M (|domain#M| b) (|contents#M| l)))))
+(declare-fun $EmptyValueArray () T@R)
+(declare-fun m (T@$Value) |T@[Int]$Value|)
+(declare-fun $IsEqual_stratified (T@$Value T@$Value) Bool)
+(declare-fun sel (|T@[Int]$Value| Int) T@$Value)
+(declare-fun st (|T@[Int]$Value| Int T@$Value) |T@[Int]$Value|)
+(assert (forall ((?x0 |T@[Int]$Value|) (?x1 Int) (?x2 T@$Value)) (= ?x2 (sel (st ?x0 ?x1 ?x2) ?x1))))
+(assert (forall ((?x0 |T@[Int]$Value|) (?x1 Int) (?y1 Int) (?x2 T@$Value)) (= (sel ?x0 ?y1) (sel (st ?x0 ?x1 ?x2) ?y1))))
+(declare-fun $LibraAccount_T_type_value () T@$TypeValue)
+(declare-fun s (l T@$Location) T@$Value)
+(declare-fun $Event_EventHandleGenerator_counter () Int)
+(declare-fun $Event_EventHandleGenerator_type_value () T@$TypeValue)
+(assert (= 0 (|l#R| $EmptyValueArray)))
+(assert (forall ((v1 T@$Value) (v2 T@$Value)) (= ($IsEqual_stratified v1 v2) (or (= v1 v2) (forall ((i Int)) (or (> 0 i) (>= i (|l#R| (|v#V| v1))) ($IsEqual_stratified (sel (|v#R| (|v#V| v1)) i) (sel (|v#R| (|v#V| v2)) i))))))))
+(assert (forall ((m@@0 T@M) (a@@0 T@$Value)) (! (or (not (is-D a@@0)) (and (is-I (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| a@@0))))) $Event_EventHandleGenerator_counter)) (forall ((x@@10 Int)) (or (> x@@10 0) (= E (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $LibraAccount_T_type_value (|a#D| a@@0))))) x@@10)))))) :qid :skolemid)))
+(declare-fun |Select_[$Location]$bool| (b T@$Location) Bool)
+(declare-fun $m@@0 () T@M)
+(declare-fun $abort_flag@2 () Bool)
+(declare-fun $m@3 () T@M)
+(declare-fun mv () T@$TypeValue)
+(declare-fun inline$$MoveToRaw$0$a@0 () Int)
+(declare-fun |Store_[$Location]$bool| (b T@$Location Bool) b)
+(assert (forall ((?x0 b) (?x1 T@$Location) (?y1 T@$Location) (?x2 Bool)) (or (= ?x1 ?y1) (= (|Select_[$Location]$bool| ?x0 ?y1) (|Select_[$Location]$bool| (|Store_[$Location]$bool| ?x0 ?x1 ?x2) ?y1)))))
+(declare-fun inline$$MoveToRaw$0$l@1 () T@$Location)
+(declare-fun |Store_[$Location]$Value| (l T@$Location T@$Value) l)
+(assert (forall ((?x0 l) (?x1 T@$Location) (?x2 T@$Value)) (= ?x2 (s (|Store_[$Location]$Value| ?x0 ?x1 ?x2) ?x1))))
+(assert (forall ((?x0 l) (?x1 T@$Location) (?y1 T@$Location) (?x2 T@$Value)) (= (s ?x0 ?y1) (s (|Store_[$Location]$Value| ?x0 ?x1 ?x2) ?y1))))
+(declare-fun inline$$Event_EventHandleGenerator_pack$0$$struct@1 () T@$Value)
+(declare-fun inline$$Event_publish_generator$0$$tmp@1 () T@$Value)
+(declare-fun i () T@$Value)
+(assert (and (not $abort_flag@2) (= inline$$Event_publish_generator$0$$tmp@1 (I 0)) (|b#$Boolean| ($Boolean (forall ((addr@@9 T@$Value)) (or (is-D addr@@9) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@9))))))))))) (or (not (=> $abort_flag@2 (|b#$Boolean| ($Boolean (forall ((addr@@4 T@$Value)) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@4)))))))))))))))) (and (= inline$$Event_EventHandleGenerator_pack$0$$struct@1 (V (R (st (st (m E) 0 inline$$Event_publish_generator$0$$tmp@1) 1 i) 1))) (not (=> (= inline$$MoveToRaw$0$a@0 (|a#D| i)) (= inline$$MoveToRaw$0$l@1 (G mv inline$$MoveToRaw$0$a@0)) (or (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| i))))) (not (= $m@3 (M (|Store_[$Location]$bool| (|domain#M| $m@@0) inline$$MoveToRaw$0$l@1 true) (|Store_[$Location]$Value| (|contents#M| $m@@0) inline$$MoveToRaw$0$l@1 inline$$Event_EventHandleGenerator_pack$0$$struct@1)))) (and (|b#$Boolean| ($Boolean ($IsEqual_stratified (s (|contents#M| $m@@0) (G mv (|a#D| i))) (V (R (|v#R| (R (|v#R| $EmptyValueArray) 0)) 1))))) (or (not (|b#$Boolean| ($Boolean ($IsEqual_stratified (s (|contents#M| $m@@0) (G mv (|a#D| i))) (V (R (|v#R| (R (st (|v#R| $EmptyValueArray) (|l#R| $EmptyValueArray) (I 0)) 1)) 0)))))) (and (|b#$Boolean| ($Boolean (forall ((addr@@1 T@$Value)) (|b#$Boolean| ($Boolean (or (not (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@1)))))) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean ($IsEqual_stratified (sel (|v#R| (|v#V| (s (|contents#M| $m@3) (G mv (|a#D| addr@@1))))) $Event_EventHandleGenerator_counter) (sel (|v#R| (|v#V| (s (|contents#M| $m@@0) (G mv (|a#D| addr@@1))))) $Event_EventHandleGenerator_counter)))))))))))) (|b#$Boolean| ($Boolean (forall ((addr@@3 T@$Value)) (|b#$Boolean| ($Boolean (or (|b#$Boolean| ($Boolean ($IsEqual_stratified (I 0) (sel (|v#R| (|v#V| (s (|contents#M| $m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| addr@@3))))) $Event_EventHandleGenerator_counter)))) (not (|b#$Boolean| ($Boolean (and (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@3) (G mv (|a#D| addr@@3))))) (|b#$Boolean| ($Boolean (not (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G $LibraAccount_T_type_value (|a#D| addr@@3))))))))))))))))))))))))))))
+(check-sat)
diff --git a/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2 b/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2
new file mode 100644
index 000000000..7f2e3084f
--- /dev/null
+++ b/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2
@@ -0,0 +1,41 @@
+; COMMAND-LINE: --ee-mode=distributed --no-check-unsat-cores
+; COMMAND-LINE: --ee-mode=central --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((dA 0)) (((A))))
+(declare-datatypes ((Loc 0)) (((G (g dA) (ag Int)))))
+(declare-sort v 0)
+(declare-datatypes ((T 0) (U 0)) (((E) (I (ii Int)) (D (d Int)) (V (vv U))) ((R (rr v)))))
+(declare-sort b 0)
+(declare-sort l 0)
+(declare-datatypes ((T@M 0)) (((M (dom b) (cnt l)))))
+(declare-fun e () U)
+(declare-fun m (T) v)
+(declare-fun iseq (T T) Bool)
+(declare-fun sel (v Int) T)
+(declare-fun st (v) v)
+(declare-fun s (l Loc) T)
+(declare-fun sb (Loc) Bool)
+(declare-fun m0 () T@M)
+(declare-fun a () Bool)
+(declare-fun im () Loc)
+(declare-fun o (Loc T) l)
+(declare-fun i () T)
+(assert (forall ((?x0 v) (?x1 Int) (?x2 T)) (= ?x2 (sel (st ?x0) ?x1))))
+(assert (forall ((v1 T) (v2 T)) (= (iseq v1 v2) (forall ((i Int)) (iseq (sel (rr (vv v1)) i) (sel (rr (vv v2)) i))))))
+(assert (forall ((?x1 Loc) (?x2 T)) (= ?x2 (s (o ?x1 ?x2) ?x1))))
+(assert (and 
+(not a) 
+(forall ((?a9 T)) (or (is-D ?a9) (sb (G A (d ?a9))))) 
+(or 
+(not (=> a (forall (($a T)) (sb (G A (d $a)))))) 
+(and 
+  (not (sb (G A (d i))))
+  (= im (G A (d (I 0)))) 
+  (= m0 (M (dom m0) (o im (V (R (st (m E))))))) 
+  (iseq (s (cnt m0) (G A (d i))) (V (R (rr e)))) 
+  (or 
+    (exists ((?a1 T)) (not (iseq (sel (rr (vv (s (cnt m0) (G A (d ?a1))))) 0) (sel (rr (vv (s (cnt m0) (G A (d ?a1))))) 0)))) 
+    (forall ((?a3 T)) (sb (G A (d ?a3)))))))))
+(check-sat)