diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-04-22 07:06:24 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-22 07:06:24 -0500 |
commit | da73f99910a25fca342c0ba1d8ec19de6c3cefda (patch) | |
tree | 724e6b2b3061b2eb57f0814537bfb2d687947e40 /test/regress/regress0 | |
parent | 2a38d482462fdf30376c984e7a82c99d08e75f92 (diff) |
Convert V2.5 SMT regressions to V2.6. (#4319)
This commit converts all v2.5 smt2 regressions to v2.6 (except for regress/regress0/lang_opts_2_5.smt2).
Diffstat (limited to 'test/regress/regress0')
13 files changed, 136 insertions, 147 deletions
diff --git a/test/regress/regress0/bug484.smt2 b/test/regress/regress0/bug484.smt2 index 87a8696b6..3b84b7aff 100644 --- a/test/regress/regress0/bug484.smt2 +++ b/test/regress/regress0/bug484.smt2 @@ -1,64 +1,63 @@ -; COMMAND-LINE: --lang=smt2.5 ; EXPECT: sat ; Preamble -------------- (set-logic ALL) (set-info :status sat) -(declare-datatypes () ((UNIT (Unit)))) -(declare-datatypes () ((BOOL (Truth) (Falsity)))) +(declare-datatypes ((UNIT 0)) (((Unit)))) +(declare-datatypes ((BOOL 0)) (((Truth) (Falsity)))) ; Decls -------------- (declare-sort A 0) (declare-sort B 0) (declare-sort C 0) (declare-sort D 0) -(declare-datatypes () ((E (one) (two) (three)))) -(declare-datatypes () ((F (four) (five) (six)))) -(declare-datatypes () ((G (c_G (seven BOOL))))) +(declare-datatypes ((E 0)) (((one) (two) (three)))) +(declare-datatypes ((F 0)) (((four) (five) (six)))) +(declare-datatypes ((G 0)) (((c_G (seven BOOL))))) -(declare-datatypes () - ((H - (c_H - (foo1 BOOL) - (foo2 A) - (foo3 B) - (foo4 B) +(declare-datatypes ((H 0)) + (( + (c_H + (foo1 BOOL) + (foo2 A) + (foo3 B) + (foo4 B) (foo5 Int) ) )) ) -(declare-datatypes () - ((I - (c_I - (bar1 E) - (bar2 Int) - (bar3 Int) +(declare-datatypes ((I 0)) + (( + (c_I + (bar1 E) + (bar2 Int) + (bar3 Int) (bar4 A) ) )) ) -(declare-datatypes () - ((J - (c_J - (f1 BOOL) - (f2 Int) - (f3 Int) - (f4 Int) - (f5 I) - (f6 B) +(declare-datatypes ((J 0)) + (( + (c_J + (f1 BOOL) + (f2 Int) + (f3 Int) + (f4 Int) + (f5 I) + (f6 B) (f7 C) ) )) ) -(declare-datatypes () - ((K - (c_K - (g1 BOOL) - (g2 F) - (g3 A) +(declare-datatypes ((K 0)) + (( + (c_K + (g1 BOOL) + (g2 F) + (g3 A) (g4 BOOL) ) )) @@ -76,39 +75,39 @@ ; Asserts -------------- -(assert - (not - (= - (ite - (=> +(assert + (not + (= + (ite + (=> (= y (g3 (select e1 x))) - (=> - (= s2 - (store - s1 - y + (=> + (= s2 + (store + s1 + y (let ((z (select s1 y))) - (c_J - (f1 z) - (f2 z) - (- (f3 (select s1 y)) 1) + (c_J + (f1 z) + (f2 z) + (- (f3 (select s1 y)) 1) (f4 z) - (f5 z) - (f6 z) + (f5 z) + (f6 z) (f7 z) ) ) ) - ) + ) (forall ((s A)) (= (g3 (select e2 s)) s)) ) ) - Truth + Truth Falsity - ) + ) Truth ) ) ) - + (check-sat) diff --git a/test/regress/regress0/bug541.smt2 b/test/regress/regress0/bug541.smt2 index 771fbed4f..1847a9111 100644 --- a/test/regress/regress0/bug541.smt2 +++ b/test/regress/regress0/bug541.smt2 @@ -1,7 +1,6 @@ -; COMMAND-LINE: --lang=smt2.5 ; EXPECT: unsat (set-logic ALL_SUPPORTED) -(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) +(declare-datatypes ((Pair 2)) ((par (T1 T2) ((mk-pair (first T1) (second T2)))))) (assert (= (mk-pair 0.0 0.0) (mk-pair 1.5 2.5))) (check-sat) (exit) diff --git a/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 index 74b836b47..1c2f22275 100644 --- a/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 +++ b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --lang=smt2.5 ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) @@ -10,22 +9,22 @@ (declare-sort T!14 0) -(declare-datatypes () ( -(LazyConQ!5 - (Lazyarg1!5 (carry!37 Conc!6) (srear!9 LazyConQ!5)) - (Lazyarg2!5 (t!270 ConQ!6)) - (Lazyarg3!5 (carry!38 Conc!6) (t!271 ConQ!6)) - (Lazyarg4!5 (tree!19 Conc!6) (carry!39 Conc!6)) - (Lazyarg5!5 (tree!20 Conc!6) (carry!40 Conc!6)) - (PushLeft!5 (ys!22 Conc!6) (xs!60 LazyConQ!5)) - (PushLeftLazy!5 (ys!23 Conc!6) (xs!61 LazyConQ!5))) -(Conc!6 - (CC!5 (left!9 Conc!6) (right!9 Conc!6)) - (Empty!5) - (Single!5 (x!106 T!14))) -(ConQ!6 - (Spine!5 (head!10 Conc!6) (rear!5 LazyConQ!5)) - (Tip!5 (t!272 Conc!6))) +(declare-datatypes ((LazyConQ!5 0) (Conc!6 0) (ConQ!6 0)) ( +( + (Lazyarg1!5 (carry!37 Conc!6) (srear!9 LazyConQ!5)) + (Lazyarg2!5 (t!270 ConQ!6)) + (Lazyarg3!5 (carry!38 Conc!6) (t!271 ConQ!6)) + (Lazyarg4!5 (tree!19 Conc!6) (carry!39 Conc!6)) + (Lazyarg5!5 (tree!20 Conc!6) (carry!40 Conc!6)) + (PushLeft!5 (ys!22 Conc!6) (xs!60 LazyConQ!5)) + (PushLeftLazy!5 (ys!23 Conc!6) (xs!61 LazyConQ!5))) +( + (CC!5 (left!9 Conc!6) (right!9 Conc!6)) + (Empty!5) + (Single!5 (x!106 T!14))) +( + (Spine!5 (head!10 Conc!6) (rear!5 LazyConQ!5)) + (Tip!5 (t!272 Conc!6))) )) (declare-fun e!41 () LazyConQ!5) @@ -46,7 +45,7 @@ (assert (=> b!40 (= e!42 e!41))) -(assert (=> b!40 (= b!39 (is-Spine!5 (evalLazyConQ2!7 l!2))))) +(assert (=> b!40 (= b!39 ((_ is Spine!5) (evalLazyConQ2!7 l!2))))) (declare-fun b!41 () Bool) diff --git a/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 b/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 index 7a0fa30c7..abcff3ddb 100644 --- a/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 +++ b/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 @@ -1,8 +1,7 @@ -; COMMAND-LINE: --lang=smt2.5 ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) -(declare-datatypes (T S) ( (Pair (pair (first T) (second S)) ) ) ) +(declare-datatypes ((Pair 2)) ((par (T S) ((pair (first T) (second S)))))) (declare-fun p1 () (Pair Bool Bool)) (declare-fun p2 () (Pair Bool Bool)) diff --git a/test/regress/regress0/datatypes/example-dailler-min.smt2 b/test/regress/regress0/datatypes/example-dailler-min.smt2 index 5702cb04b..b8e077c1d 100644 --- a/test/regress/regress0/datatypes/example-dailler-min.smt2 +++ b/test/regress/regress0/datatypes/example-dailler-min.smt2 @@ -1,8 +1,7 @@ -; COMMAND-LINE: --lang=smt2.5 ; EXPECT: sat (set-logic ALL) (set-info :status sat) -(declare-datatypes () ((D (C (R Bool))))) +(declare-datatypes ((D 0)) (((C (R Bool))))) (declare-fun a () (Array Int D)) (declare-fun P ((Array Int D)) Bool) (assert (P a)) diff --git a/test/regress/regress0/datatypes/pair-real-bool.smt2 b/test/regress/regress0/datatypes/pair-real-bool.smt2 index a4d5ff0ec..c29eeb4e9 100644 --- a/test/regress/regress0/datatypes/pair-real-bool.smt2 +++ b/test/regress/regress0/datatypes/pair-real-bool.smt2 @@ -1,21 +1,20 @@ -; COMMAND-LINE: --lang=smt2.5 ; EXPECT: sat ;(set-option :produce-models true) (set-logic QF_ALL_SUPPORTED) (set-info :status sat) -(declare-datatypes () ( - ( RealTree - ( Node - (left RealTree) - (elem Real) - (right RealTree)) +(declare-datatypes ((RealTree 0)) ( + ( + (Node + (left RealTree) + (elem Real) + (right RealTree)) (Leaf) ) )) -(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) +(declare-datatypes ((Pair 2)) ((par (T1 T2) ((mk-pair (first T1) (second T2)))))) -( declare-fun SumeAndPositiveTree ( RealTree ) (Pair Real Bool) ) +(declare-fun SumeAndPositiveTree (RealTree) (Pair Real Bool)) (declare-fun l1 () RealTree) (declare-fun l2 () RealTree) diff --git a/test/regress/regress0/fmf/sc_bad_model_1221.smt2 b/test/regress/regress0/fmf/sc_bad_model_1221.smt2 index 68a4399ca..d951e6c50 100644 --- a/test/regress/regress0/fmf/sc_bad_model_1221.smt2 +++ b/test/regress/regress0/fmf/sc_bad_model_1221.smt2 @@ -1,33 +1,33 @@ -; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; COMMAND-LINE: --finite-model-find ; EXPECT: sat - (set-logic ALL_SUPPORTED) - (set-info :status sat) - (declare-sort a 0) - (declare-fun __nun_card_witness_0 () a) - (declare-datatypes () ((prod (Pair (_select_Pair_0 a) (_select_Pair_1 a))))) - (declare-sort G_snd 0) - (declare-fun __nun_card_witness_1 () G_snd) - (declare-fun snd (prod) a) - (declare-fun proj_G_snd_0 (G_snd) prod) - (assert - (forall ((a/32 G_snd)) - (and - (= (snd (proj_G_snd_0 a/32)) (_select_Pair_1 (proj_G_snd_0 a/32))) - true))) - (declare-fun p () prod) - (declare-datatypes () ((pd (Pd (_select_Pd_0 prod))))) - (declare-sort G_fs 0) - (declare-fun __nun_card_witness_2 () G_fs) - (declare-fun fs (pd) a) - (declare-fun proj_G_fs_0 (G_fs) pd) - (assert - (forall ((a/33 G_fs)) - (and - (= (fs (proj_G_fs_0 a/33)) - (_select_Pair_0 (_select_Pd_0 (proj_G_fs_0 a/33)))) - true))) - (assert - (and (not (= (fs (Pd p)) (snd p))) - (exists ((a/34 G_fs)) (= (Pd p) (proj_G_fs_0 a/34))) - (exists ((a/35 G_snd)) (= p (proj_G_snd_0 a/35))))) - (check-sat) +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-sort a 0) +(declare-fun __nun_card_witness_0 () a) +(declare-datatypes ((prod 0)) (((Pair (_select_Pair_0 a) (_select_Pair_1 a))))) +(declare-sort G_snd 0) +(declare-fun __nun_card_witness_1 () G_snd) +(declare-fun snd (prod) a) +(declare-fun proj_G_snd_0 (G_snd) prod) +(assert + (forall ((a/32 G_snd)) + (and + (= (snd (proj_G_snd_0 a/32)) (_select_Pair_1 (proj_G_snd_0 a/32))) + true))) +(declare-fun p () prod) +(declare-datatypes ((pd 0)) (((Pd (_select_Pd_0 prod))))) +(declare-sort G_fs 0) +(declare-fun __nun_card_witness_2 () G_fs) +(declare-fun fs (pd) a) +(declare-fun proj_G_fs_0 (G_fs) pd) +(assert + (forall ((a/33 G_fs)) + (and + (= (fs (proj_G_fs_0 a/33)) + (_select_Pair_0 (_select_Pd_0 (proj_G_fs_0 a/33)))) + true))) +(assert + (and (not (= (fs (Pd p)) (snd p))) + (exists ((a/34 G_fs)) (= (Pd p) (proj_G_fs_0 a/34))) + (exists ((a/35 G_snd)) (= p (proj_G_snd_0 a/35))))) +(check-sat) diff --git a/test/regress/regress0/issue1063-overloading-dt-cons.smt2 b/test/regress/regress0/issue1063-overloading-dt-cons.smt2 index f8ca2a9e5..a77fcdd22 100644 --- a/test/regress/regress0/issue1063-overloading-dt-cons.smt2 +++ b/test/regress/regress0/issue1063-overloading-dt-cons.smt2 @@ -1,14 +1,13 @@ -; COMMAND-LINE: --lang=smt2.5 ; EXPECT: sat (set-logic ALL) (set-info :status sat) -(declare-datatypes () ((Enum0 (In_Air) (On_Ground) (None)))) -(declare-datatypes () ((Enum1 (True) (False) (None)))) +(declare-datatypes ((Enum0 0)) (((In_Air) (On_Ground) (None)))) +(declare-datatypes ((Enum1 0)) (((True) (False) (None)))) (declare-fun var_0 (Int) Enum0) (declare-fun var_1 (Int) Enum1) (assert (= (var_0 0) (as None Enum0))) (assert (= (var_1 1) (as None Enum1))) -(assert (not (is-In_Air (var_0 0)))) +(assert (not ((_ is In_Air) (var_0 0)))) (declare-fun var_2 () Enum1) -(assert (is-None var_2)) +(assert ((_ is (as None Enum1)) var_2)) (check-sat) diff --git a/test/regress/regress0/issue1063-overloading-dt-fun.smt2 b/test/regress/regress0/issue1063-overloading-dt-fun.smt2 index 9cae20647..f9c326114 100644 --- a/test/regress/regress0/issue1063-overloading-dt-fun.smt2 +++ b/test/regress/regress0/issue1063-overloading-dt-fun.smt2 @@ -1,8 +1,7 @@ -; COMMAND-LINE: --lang=smt2.5 ; EXPECT: sat (set-logic ALL) (set-info :status sat) -(declare-datatypes () ((Enum (cons (val Int)) (On_Ground) (None)))) +(declare-datatypes ((Enum 0)) (((cons (val Int)) (On_Ground) (None)))) (declare-fun cons (Int Int) Int) (declare-fun cons (Enum) Bool) (declare-fun cons (Bool) Int) diff --git a/test/regress/regress0/issue1063-overloading-dt-sel.smt2 b/test/regress/regress0/issue1063-overloading-dt-sel.smt2 index b3316d373..390c9acad 100644 --- a/test/regress/regress0/issue1063-overloading-dt-sel.smt2 +++ b/test/regress/regress0/issue1063-overloading-dt-sel.smt2 @@ -1,9 +1,8 @@ -; COMMAND-LINE: --lang=smt2.5 ; EXPECT: sat (set-logic ALL) (set-info :status sat) -(declare-datatypes () ((Enum0 (cons (data Int)) (None)))) -(declare-datatypes () ((Enum1 (cons (data Bool)) (None)))) +(declare-datatypes ((Enum0 0)) (((cons (data Int)) (None)))) +(declare-datatypes ((Enum1 0)) (((cons (data Bool)) (None)))) (declare-fun var_0 () Enum0) (declare-fun var_1 () Enum1) (assert (= (data var_0) 5)) diff --git a/test/regress/regress0/push-pop/bug654-dd.smt2 b/test/regress/regress0/push-pop/bug654-dd.smt2 index 82033e606..bd8419b57 100644 --- a/test/regress/regress0/push-pop/bug654-dd.smt2 +++ b/test/regress/regress0/push-pop/bug654-dd.smt2 @@ -1,8 +1,8 @@ -; COMMAND-LINE: --incremental --fmf-fun --strings-exp --lang=smt2.5 +; COMMAND-LINE: --incremental --fmf-fun --strings-exp (set-logic ALL_SUPPORTED) -(declare-datatypes () ( -(List_T_C (List_T_C$CNil_T_CustomerType) (ListTC (ListTC$head T_CustomerType) (ListTC$tail List_T_C))) -(T_CustomerType (T_CustomerType$C_T_CustomerType (T_CustomerType$C_T_CustomerType$a_CompanyName Int) (T_CustomerType$C_T_CustomerType$a_ContactName Int) (ID Int))) +(declare-datatypes ((List_T_C 0) (T_CustomerType 0)) ( +((List_T_C$CNil_T_CustomerType) (ListTC (ListTC$head T_CustomerType) (ListTC$tail List_T_C))) +((T_CustomerType$C_T_CustomerType (T_CustomerType$C_T_CustomerType$a_CompanyName Int) (T_CustomerType$C_T_CustomerType$a_ContactName Int) (ID Int))) )) (declare-fun f (List_T_C) Bool) (declare-fun tail_uf_1 (List_T_C) List_T_C) @@ -10,13 +10,13 @@ (declare-sort U 0) (declare-fun a (U) List_T_C) (declare-fun z (U) U) -(assert -(forall ((?i U)) -(= (f (a ?i)) (not (is-ListTC (a ?i))) +(assert +(forall ((?i U)) +(= (f (a ?i)) (not ((_ is ListTC) (a ?i))) ))) -(assert -(forall ((?i U)) -(= (a (z ?i)) (tail_uf_1 (a ?i)))) ) +(assert +(forall ((?i U)) +(= (a (z ?i)) (tail_uf_1 (a ?i)))) ) ; EXPECT: sat (push 1) (check-sat) diff --git a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 index 7e58ea87c..a39aa4ef5 100644 --- a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 +++ b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --cegqi --dt-rewrite-error-sel --lang=smt2.5 +; COMMAND-LINE: --cegqi --dt-rewrite-error-sel ; EXPECT: unsat (set-logic ALL_SUPPORTED) -(declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) +(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) (assert (exists ((y Int)) (forall ((x List)) (not (= (head x) (+ y 7)))))) (check-sat) diff --git a/test/regress/regress0/quantifiers/rew-to-scala.smt2 b/test/regress/regress0/quantifiers/rew-to-scala.smt2 index 6c191d688..343458bee 100644 --- a/test/regress/regress0/quantifiers/rew-to-scala.smt2 +++ b/test/regress/regress0/quantifiers/rew-to-scala.smt2 @@ -1,15 +1,13 @@ -; COMMAND-LINE: --lang=smt2.5 ; EXPECT: unsat (set-logic ALL_SUPPORTED) (set-info :status unsat) -(declare-datatypes () ((Formula!953 (And!954 (lhs!955 Formula!953) (rhs!956 Formula!953)) (Not!957 (f!958 Formula!953)) (Or!959 (lhs!960 Formula!953) (rhs!961 Formula!953)) (Variable!962 (id!963 (_ BitVec 32)))) -)) +(declare-datatypes ((Formula!953 0)) (((And!954 (lhs!955 Formula!953) (rhs!956 Formula!953)) (Not!957 (f!958 Formula!953)) (Or!959 (lhs!960 Formula!953) (rhs!961 Formula!953)) (Variable!962 (id!963 (_ BitVec 32)))))) (declare-fun error_value!964 () Bool) (declare-fun isNNF!208 (Formula!953) Bool) (declare-fun error_value!965 () Formula!953) (declare-fun nnf!206 (Formula!953) Formula!953) (declare-fun error_value!966 () Formula!953) -(assert (forall ((f!207 Formula!953)) (= (isNNF!208 f!207) (ite (is-And!954 f!207) (and (and (isNNF!208 (lhs!955 f!207)) (isNNF!208 (lhs!955 f!207))) (isNNF!208 (rhs!956 f!207))) (ite (is-Or!959 f!207) (and (and (isNNF!208 (lhs!960 f!207)) (isNNF!208 (lhs!960 f!207))) (isNNF!208 (rhs!961 f!207))) (ite (is-Not!957 f!207) false (ite (is-Variable!962 f!207) true error_value!964))))) )) -(assert (forall ((formula!205 Formula!953)) (= (nnf!206 formula!205) (ite (is-And!954 formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite (is-Or!959 formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-And!954 (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Or!959 (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Not!957 (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite (is-Not!957 formula!205) formula!205 (ite (is-Variable!962 formula!205) formula!205 error_value!965)))))))) )) -(assert (exists ((formula!205 Formula!953)) (not (=> (is-Variable!962 formula!205) (isNNF!208 (ite (is-And!954 formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite (is-Or!959 formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-And!954 (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Or!959 (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Not!957 (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite (is-Not!957 formula!205) formula!205 (ite (is-Variable!962 formula!205) formula!205 error_value!966)))))))))) )) +(assert (forall ((f!207 Formula!953)) (= (isNNF!208 f!207) (ite ((_ is And!954) f!207) (and (and (isNNF!208 (lhs!955 f!207)) (isNNF!208 (lhs!955 f!207))) (isNNF!208 (rhs!956 f!207))) (ite ((_ is Or!959) f!207) (and (and (isNNF!208 (lhs!960 f!207)) (isNNF!208 (lhs!960 f!207))) (isNNF!208 (rhs!961 f!207))) (ite ((_ is Not!957) f!207) false (ite ((_ is Variable!962) f!207) true error_value!964))))) )) +(assert (forall ((formula!205 Formula!953)) (= (nnf!206 formula!205) (ite ((_ is And!954) formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite ((_ is Or!959) formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and ((_ is Not!957) formula!205) ((_ is Not!957) formula!205)) ((_ is And!954) (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and ((_ is Not!957) formula!205) ((_ is Not!957) formula!205)) ((_ is Or!959) (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and ((_ is Not!957) formula!205) ((_ is Not!957) formula!205)) ((_ is Not!957) (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite ((_ is Not!957) formula!205) formula!205 (ite ((_ is Variable!962) formula!205) formula!205 error_value!965)))))))) )) +(assert (exists ((formula!205 Formula!953)) (not (=> ((_ is Variable!962) formula!205) (isNNF!208 (ite ((_ is And!954) formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite ((_ is Or!959) formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and ((_ is Not!957) formula!205) ((_ is Not!957) formula!205)) ((_ is And!954) (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and ((_ is Not!957) formula!205) ((_ is Not!957) formula!205)) ((_ is Or!959) (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and ((_ is Not!957) formula!205) ((_ is Not!957) formula!205)) ((_ is Not!957) (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite ((_ is Not!957) formula!205) formula!205 (ite ((_ is Variable!962) formula!205) formula!205 error_value!966)))))))))) )) (check-sat) |