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).

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)