4 files changed, 218 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index cd79fe050..82f8f2c27 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -2,6 +2,7 @@
 equals = =
 
 REG0_TESTS = \
+	regress0/arith/apply2const-test.smt2 \
 	regress0/arith/arith.01.cvc \
 	regress0/arith/arith.02.cvc \
 	regress0/arith/arith.03.cvc \
@@ -437,6 +438,7 @@ REG0_TESTS = \
 	regress0/fmf/syn002-si-real-int.smt2 \
 	regress0/fmf/tail_rec.smt2 \
 	regress0/fp/simple.smt2 \
+	regress0/fp/ext-rew-test.smt2 \
 	regress0/fuzz_1.smt \
 	regress0/fuzz_3.smt \
 	regress0/get-value-incremental.smt2 \
@@ -495,6 +497,7 @@ REG0_TESTS = \
 	regress0/logops.04.cvc \
 	regress0/logops.05.cvc \
 	regress0/nl/coeff-sat.smt2 \
+	regress0/nl/ext-rew-aggr-test.smt2 \
 	regress0/nl/magnitude-wrong-1020-m.smt2 \
 	regress0/nl/mult-po.smt2 \
 	regress0/nl/nia-wrong-tl.smt2 \
diff --git a/test/regress/regress0/arith/apply2const-test.smt2 b/test/regress/regress0/arith/apply2const-test.smt2
new file mode 100644
index 000000000..e11878a74
--- /dev/null
+++ b/test/regress/regress0/arith/apply2const-test.smt2
@@ -0,0 +1,24 @@
+; COMMAND-LINE: --rewrite-apply-to-const
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_UFLIA)
+(set-info :source | MathSat group |)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun hash_1 (Int) Int)
+(declare-fun hash_2 (Int) Int)
+(declare-fun hash_3 (Int) Int)
+(declare-fun hash_4 (Int) Int)
+(declare-fun hash_5 (Int) Int)
+(declare-fun hash_6 (Int) Int)
+(declare-fun hash_7 (Int) Int)
+(declare-fun hash_8 (Int) Int)
+(declare-fun hash_9 (Int) Int)
+(declare-fun hash_10 (Int) Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(declare-fun x4 () Int)
+(assert (let ((?v_0 (hash_1 x1)) (?v_1 (hash_1 x2)) (?v_2 (hash_1 x3)) (?v_3 (hash_1 x4)) (?v_4 (hash_2 x1)) (?v_5 (hash_2 x2)) (?v_6 (hash_2 x3)) (?v_7 (hash_2 x4)) (?v_8 (hash_3 x1)) (?v_9 (hash_3 x2)) (?v_10 (hash_3 x3)) (?v_11 (hash_3 x4)) (?v_12 (hash_4 x1)) (?v_13 (hash_4 x2)) (?v_14 (hash_4 x3)) (?v_15 (hash_4 x4)) (?v_16 (hash_5 x1)) (?v_17 (hash_5 x2)) (?v_18 (hash_5 x3)) (?v_19 (hash_5 x4)) (?v_20 (hash_6 x1)) (?v_21 (hash_6 x2)) (?v_22 (hash_6 x3)) (?v_23 (hash_6 x4)) (?v_24 (hash_7 x1)) (?v_25 (hash_7 x2)) (?v_26 (hash_7 x3)) (?v_27 (hash_7 x4)) (?v_28 (hash_8 x1)) (?v_29 (hash_8 x2)) (?v_30 (hash_8 x3)) (?v_31 (hash_8 x4)) (?v_32 (hash_9 x1)) (?v_33 (hash_9 x2)) (?v_34 (hash_9 x3)) (?v_35 (hash_9 x4)) (?v_36 (hash_10 x1)) (?v_37 (hash_10 x2)) (?v_38 (hash_10 x3)) (?v_39 (hash_10 x4))) (let ((?v_40 (= ?v_0 ?v_4))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (distinct ?v_0 ?v_1) (distinct ?v_0 ?v_2)) (distinct ?v_0 ?v_3)) (distinct ?v_1 ?v_2)) (distinct ?v_1 ?v_3)) (distinct ?v_2 ?v_3)) (distinct ?v_4 ?v_5)) (distinct ?v_4 ?v_6)) (distinct ?v_4 ?v_7)) (distinct ?v_5 ?v_6)) (distinct ?v_5 ?v_7)) (distinct ?v_6 ?v_7)) (distinct ?v_8 ?v_9)) (distinct ?v_8 ?v_10)) (distinct ?v_8 ?v_11)) (distinct ?v_9 ?v_10)) (distinct ?v_9 ?v_11)) (distinct ?v_10 ?v_11)) (distinct ?v_12 ?v_13)) (distinct ?v_12 ?v_14)) (distinct ?v_12 ?v_15)) (distinct ?v_13 ?v_14)) (distinct ?v_13 ?v_15)) (distinct ?v_14 ?v_15)) (distinct ?v_16 ?v_17)) (distinct ?v_16 ?v_18)) (distinct ?v_16 ?v_19)) (distinct ?v_17 ?v_18)) (distinct ?v_17 ?v_19)) (distinct ?v_18 ?v_19)) (distinct ?v_20 ?v_21)) (distinct ?v_20 ?v_22)) (distinct ?v_20 ?v_23)) (distinct ?v_21 ?v_22)) (distinct ?v_21 ?v_23)) (distinct ?v_22 ?v_23)) (distinct ?v_24 ?v_25)) (distinct ?v_24 ?v_26)) (distinct ?v_24 ?v_27)) (distinct ?v_25 ?v_26)) (distinct ?v_25 ?v_27)) (distinct ?v_26 ?v_27)) (distinct ?v_28 ?v_29)) (distinct ?v_28 ?v_30)) (distinct ?v_28 ?v_31)) (distinct ?v_29 ?v_30)) (distinct ?v_29 ?v_31)) (distinct ?v_30 ?v_31)) (distinct ?v_32 ?v_33)) (distinct ?v_32 ?v_34)) (distinct ?v_32 ?v_35)) (distinct ?v_33 ?v_34)) (distinct ?v_33 ?v_35)) (distinct ?v_34 ?v_35)) (distinct ?v_36 ?v_37)) (distinct ?v_36 ?v_38)) (distinct ?v_36 ?v_39)) (distinct ?v_37 ?v_38)) (distinct ?v_37 ?v_39)) (distinct ?v_38 ?v_39)) (or (or (or (= ?v_0 x1) (= ?v_0 x2)) (= ?v_0 x3)) (= ?v_0 x4))) (or (or (or (= ?v_1 x1) (= ?v_1 x2)) (= ?v_1 x3)) (= ?v_1 x4))) (or (or (or (= ?v_2 x1) (= ?v_2 x2)) (= ?v_2 x3)) (= ?v_2 x4))) (or (or (or (= ?v_3 x1) (= ?v_3 x2)) (= ?v_3 x3)) (= ?v_3 x4))) (or (or (or (= ?v_4 x1) (= ?v_4 x2)) (= ?v_4 x3)) (= ?v_4 x4))) (or (or (or (= ?v_5 x1) (= ?v_5 x2)) (= ?v_5 x3)) (= ?v_5 x4))) (or (or (or (= ?v_6 x1) (= ?v_6 x2)) (= ?v_6 x3)) (= ?v_6 x4))) (or (or (or (= ?v_7 x1) (= ?v_7 x2)) (= ?v_7 x3)) (= ?v_7 x4))) (or (or (or (= ?v_8 x1) (= ?v_8 x2)) (= ?v_8 x3)) (= ?v_8 x4))) (or (or (or (= ?v_9 x1) (= ?v_9 x2)) (= ?v_9 x3)) (= ?v_9 x4))) (or (or (or (= ?v_10 x1) (= ?v_10 x2)) (= ?v_10 x3)) (= ?v_10 x4))) (or (or (or (= ?v_11 x1) (= ?v_11 x2)) (= ?v_11 x3)) (= ?v_11 x4))) (or (or (or (= ?v_12 x1) (= ?v_12 x2)) (= ?v_12 x3)) (= ?v_12 x4))) (or (or (or (= ?v_13 x1) (= ?v_13 x2)) (= ?v_13 x3)) (= ?v_13 x4))) (or (or (or (= ?v_14 x1) (= ?v_14 x2)) (= ?v_14 x3)) (= ?v_14 x4))) (or (or (or (= ?v_15 x1) (= ?v_15 x2)) (= ?v_15 x3)) (= ?v_15 x4))) (or (or (or (= ?v_16 x1) (= ?v_16 x2)) (= ?v_16 x3)) (= ?v_16 x4))) (or (or (or (= ?v_17 x1) (= ?v_17 x2)) (= ?v_17 x3)) (= ?v_17 x4))) (or (or (or (= ?v_18 x1) (= ?v_18 x2)) (= ?v_18 x3)) (= ?v_18 x4))) (or (or (or (= ?v_19 x1) (= ?v_19 x2)) (= ?v_19 x3)) (= ?v_19 x4))) (or (or (or (= ?v_20 x1) (= ?v_20 x2)) (= ?v_20 x3)) (= ?v_20 x4))) (or (or (or (= ?v_21 x1) (= ?v_21 x2)) (= ?v_21 x3)) (= ?v_21 x4))) (or (or (or (= ?v_22 x1) (= ?v_22 x2)) (= ?v_22 x3)) (= ?v_22 x4))) (or (or (or (= ?v_23 x1) (= ?v_23 x2)) (= ?v_23 x3)) (= ?v_23 x4))) (or (or (or (= ?v_24 x1) (= ?v_24 x2)) (= ?v_24 x3)) (= ?v_24 x4))) (or (or (or (= ?v_25 x1) (= ?v_25 x2)) (= ?v_25 x3)) (= ?v_25 x4))) (or (or (or (= ?v_26 x1) (= ?v_26 x2)) (= ?v_26 x3)) (= ?v_26 x4))) (or (or (or (= ?v_27 x1) (= ?v_27 x2)) (= ?v_27 x3)) (= ?v_27 x4))) (or (or (or (= ?v_28 x1) (= ?v_28 x2)) (= ?v_28 x3)) (= ?v_28 x4))) (or (or (or (= ?v_29 x1) (= ?v_29 x2)) (= ?v_29 x3)) (= ?v_29 x4))) (or (or (or (= ?v_30 x1) (= ?v_30 x2)) (= ?v_30 x3)) (= ?v_30 x4))) (or (or (or (= ?v_31 x1) (= ?v_31 x2)) (= ?v_31 x3)) (= ?v_31 x4))) (or (or (or (= ?v_32 x1) (= ?v_32 x2)) (= ?v_32 x3)) (= ?v_32 x4))) (or (or (or (= ?v_33 x1) (= ?v_33 x2)) (= ?v_33 x3)) (= ?v_33 x4))) (or (or (or (= ?v_34 x1) (= ?v_34 x2)) (= ?v_34 x3)) (= ?v_34 x4))) (or (or (or (= ?v_35 x1) (= ?v_35 x2)) (= ?v_35 x3)) (= ?v_35 x4))) (or (or (or (= ?v_36 x1) (= ?v_36 x2)) (= ?v_36 x3)) (= ?v_36 x4))) (or (or (or (= ?v_37 x1) (= ?v_37 x2)) (= ?v_37 x3)) (= ?v_37 x4))) (or (or (or (= ?v_38 x1) (= ?v_38 x2)) (= ?v_38 x3)) (= ?v_38 x4))) (or (or (or (= ?v_39 x1) (= ?v_39 x2)) (= ?v_39 x3)) (= ?v_39 x4))) (distinct x1 x2)) (distinct x1 x3)) (distinct x1 x4)) (distinct x2 x3)) (distinct x2 x4)) (distinct x3 x4)) (<= 0 x1)) (< x1 5)) (<= 0 x2)) (< x2 5)) (<= 0 x3)) (< x3 5)) (<= 0 x4)) (< x4 5)) (distinct (ite ?v_40 ?v_4 (+ ?v_0 ?v_0)) (ite ?v_40 ?v_4 (* 2 ?v_0)))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/fp/ext-rew-test.smt2 b/test/regress/regress0/fp/ext-rew-test.smt2
new file mode 100644
index 000000000..785c654ef
--- /dev/null
+++ b/test/regress/regress0/fp/ext-rew-test.smt2
@@ -0,0 +1,86 @@
+; COMMAND-LINE: --ext-rew-prep
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FP)
+(set-info :category "crafted")
+(set-info :source |Alberto Griggio <griggio@fbk.eu>. These benchmarks were used for the evaluation in the following paper: L. Haller, A. Griggio, M. Brain, D. Kroening: Deciding floating-point logic with systematic abstraction. FMCAD 2012. Real-numbered literals have been automatically translated by MathSAT|)
+(set-info :status unknown)
+;; MathSAT API call trace
+;; generated on 05/20/15 17:24:51
+
+(declare-fun b13 () (_ FloatingPoint 11 53))
+(declare-fun b25 () (_ FloatingPoint 11 53))
+(declare-fun b22 () (_ FloatingPoint 11 53))
+(declare-fun b82 () (_ FloatingPoint 11 53))
+(declare-fun b14 () (_ FloatingPoint 11 53))
+(declare-fun b34 () (_ FloatingPoint 11 53))
+(declare-fun b43 () (_ FloatingPoint 11 53))
+(declare-fun b85 () (_ FloatingPoint 11 53))
+(declare-fun b16 () (_ FloatingPoint 11 53))
+(declare-fun b131 () (_ FloatingPoint 11 53))
+(declare-fun b126 () (_ FloatingPoint 11 53))
+(define-fun _t_3 () RoundingMode RNE)
+(define-fun _t_9 () (_ FloatingPoint 11 53) b131)
+(define-fun _t_10 () (_ FloatingPoint 11 53) b43)
+(define-fun _t_11 () Bool (= _t_9 _t_10))
+(define-fun _t_12 () Bool (not _t_11))
+(define-fun _t_13 () (_ FloatingPoint 11 53) b126)
+(define-fun _t_14 () (_ FloatingPoint 11 53) b34)
+(define-fun _t_15 () Bool (= _t_13 _t_14))
+(define-fun _t_16 () Bool (not _t_15))
+(define-fun _t_17 () (_ FloatingPoint 11 53) b13)
+(define-fun _t_18 () (_ FloatingPoint 11 53) b25)
+(define-fun _t_19 () (_ FloatingPoint 11 53) (fp.mul _t_3 _t_17 _t_18))
+(define-fun _t_20 () (_ FloatingPoint 11 53) b16)
+(define-fun _t_21 () (_ FloatingPoint 11 53) b22)
+(define-fun _t_22 () (_ FloatingPoint 11 53) (fp.add _t_3 _t_20 _t_21))
+(define-fun _t_23 () Bool (fp.lt _t_22 _t_19))
+(define-fun _t_24 () Bool (not _t_23))
+(define-fun _t_25 () (_ FloatingPoint 11 53) b14)
+(define-fun _t_26 () (_ FloatingPoint 11 53) (fp.neg _t_25))
+(define-fun _t_27 () (_ FloatingPoint 11 53) (fp.add _t_3 _t_17 _t_26))
+(define-fun _t_28 () Bool (fp.lt _t_27 _t_21))
+(define-fun _t_29 () Bool (not _t_28))
+(define-fun _t_30 () (_ FloatingPoint 11 53) (fp.mul _t_3 _t_17 _t_25))
+(define-fun _t_31 () Bool (fp.lt _t_30 _t_20))
+(define-fun _t_32 () Bool (not _t_31))
+(define-fun _t_33 () (_ FloatingPoint 11 53) (fp.add _t_3 _t_17 _t_25))
+(define-fun _t_34 () Bool (fp.lt _t_33 _t_20))
+(define-fun _t_35 () Bool (not _t_34))
+(define-fun _t_36 () Bool (= _t_13 _t_20))
+(define-fun _t_37 () Bool (and _t_35 _t_36))
+(define-fun _t_38 () Bool (= _t_9 _t_21))
+(define-fun _t_39 () Bool (and _t_37 _t_38))
+(define-fun _t_40 () (_ FloatingPoint 11 53) b85)
+(define-fun _t_41 () Bool (fp.leq _t_40 _t_25))
+(define-fun _t_42 () Bool (and _t_39 _t_41))
+(define-fun _t_43 () (_ FloatingPoint 11 53) b82)
+(define-fun _t_44 () Bool (fp.leq _t_25 _t_43))
+(define-fun _t_45 () Bool (and _t_42 _t_44))
+(define-fun _t_46 () Bool (fp.leq _t_40 _t_17))
+(define-fun _t_47 () Bool (and _t_45 _t_46))
+(define-fun _t_48 () Bool (fp.leq _t_17 _t_43))
+(define-fun _t_49 () Bool (and _t_47 _t_48))
+(define-fun _t_50 () Bool (fp.leq _t_40 _t_20))
+(define-fun _t_51 () Bool (and _t_49 _t_50))
+(define-fun _t_52 () Bool (fp.leq _t_20 _t_43))
+(define-fun _t_53 () Bool (and _t_51 _t_52))
+(define-fun _t_54 () Bool (fp.leq _t_40 _t_21))
+(define-fun _t_55 () Bool (and _t_53 _t_54))
+(define-fun _t_56 () Bool (fp.leq _t_21 _t_43))
+(define-fun _t_57 () Bool (and _t_55 _t_56))
+(define-fun _t_58 () (_ FloatingPoint 11 53) (fp.add _t_3 _t_9 _t_13))
+(define-fun _t_59 () Bool (fp.lt _t_58 _t_19))
+(define-fun _t_60 () Bool (and _t_57 _t_59))
+(define-fun _t_61 () Bool (fp.lt _t_27 _t_9))
+(define-fun _t_62 () Bool (and _t_60 _t_61))
+(define-fun _t_63 () Bool (fp.lt _t_33 _t_13))
+(define-fun _t_64 () Bool (and _t_62 _t_63))
+(define-fun _t_65 () Bool (and _t_32 _t_64))
+(define-fun _t_66 () Bool (and _t_29 _t_65))
+(define-fun _t_67 () Bool (and _t_24 _t_66))
+(define-fun _t_68 () Bool (and _t_16 _t_67))
+(define-fun _t_69 () Bool (and _t_12 _t_68))
+(assert _t_69)
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/nl/ext-rew-aggr-test.smt2 b/test/regress/regress0/nl/ext-rew-aggr-test.smt2
new file mode 100644
index 000000000..d7a082304
--- /dev/null
+++ b/test/regress/regress0/nl/ext-rew-aggr-test.smt2
@@ -0,0 +1,105 @@
+; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NIA)
+(set-info :source |
+Generated by: Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, Albert Rubio
+Generated on: 2017-04-27
+Generator: VeryMax
+Application: Termination proving
+Target solver: barcelogic
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun global_invc1_0 () Int)
+(declare-fun lam0n0 () Int)
+(declare-fun lam0n2 () Int)
+(declare-fun global_invc1_1 () Int)
+(declare-fun lam0n1 () Int)
+(declare-fun lam1n0 () Int)
+(declare-fun lam1n1 () Int)
+(declare-fun lam1n3 () Int)
+(declare-fun lam1n4 () Int)
+(declare-fun lam1n2 () Int)
+(declare-fun term_invc1_0 () Int)
+(declare-fun lam2n0 () Int)
+(declare-fun lam2n1 () Int)
+(declare-fun lam2n3 () Int)
+(declare-fun lam2n4 () Int)
+(declare-fun lam2n5 () Int)
+(declare-fun lam2n6 () Int)
+(declare-fun lam2n7 () Int)
+(declare-fun lam2n8 () Int)
+(declare-fun lam2n9 () Int)
+(declare-fun lam2n10 () Int)
+(declare-fun lam2n11 () Int)
+(declare-fun lam2n12 () Int)
+(declare-fun lam2n13 () Int)
+(declare-fun lam2n2 () Int)
+(declare-fun term_invc1_1 () Int)
+(declare-fun non_inc1_L () Bool)
+(declare-fun lam3n0 () Int)
+(declare-fun lam3n1 () Int)
+(declare-fun lam3n3 () Int)
+(declare-fun lam3n4 () Int)
+(declare-fun lam3n5 () Int)
+(declare-fun lam3n6 () Int)
+(declare-fun lam3n7 () Int)
+(declare-fun lam3n8 () Int)
+(declare-fun lam3n9 () Int)
+(declare-fun lam3n10 () Int)
+(declare-fun lam3n11 () Int)
+(declare-fun lam3n12 () Int)
+(declare-fun lam3n13 () Int)
+(declare-fun lam3n15 () Int)
+(declare-fun lam3n14 () Int)
+(declare-fun lam3n2 () Int)
+(declare-fun rfc0 () Int)
+(declare-fun disabled1_L () Bool)
+(declare-fun bounded1_L () Bool)
+(declare-fun lam4n0 () Int)
+(declare-fun lam4n1 () Int)
+(declare-fun lam4n3 () Int)
+(declare-fun lam4n4 () Int)
+(declare-fun lam4n5 () Int)
+(declare-fun lam4n6 () Int)
+(declare-fun lam4n7 () Int)
+(declare-fun lam4n8 () Int)
+(declare-fun lam4n9 () Int)
+(declare-fun lam4n10 () Int)
+(declare-fun lam4n11 () Int)
+(declare-fun lam4n12 () Int)
+(declare-fun lam4n13 () Int)
+(declare-fun lam4n14 () Int)
+(declare-fun lam4n2 () Int)
+(declare-fun rfc1 () Int)
+(declare-fun dec1_L () Bool)
+(declare-fun lam5n0 () Int)
+(declare-fun lam5n1 () Int)
+(declare-fun lam5n3 () Int)
+(declare-fun lam5n4 () Int)
+(declare-fun lam5n5 () Int)
+(declare-fun lam5n6 () Int)
+(declare-fun lam5n7 () Int)
+(declare-fun lam5n8 () Int)
+(declare-fun lam5n9 () Int)
+(declare-fun lam5n10 () Int)
+(declare-fun lam5n11 () Int)
+(declare-fun lam5n12 () Int)
+(declare-fun lam5n13 () Int)
+(declare-fun lam5n14 () Int)
+(declare-fun lam5n2 () Int)
+(declare-fun bnd_and_dec1_L () Bool)
+(declare-fun GLOBAL_NT_1 () Bool)
+(declare-fun global_V0_1 () Int)
+(declare-fun TERM_NT_1 () Bool)
+(declare-fun term_V0_1 () Int)
+(declare-fun ALL_NON_INC_0 () Bool)
+(declare-fun DIS_OR_ALL_NON_INC_0 () Bool)
+(declare-fun SOME_BND_AND_DEC_0 () Bool)
+(declare-fun V0_NIV () Int)
+(declare-fun V1_NIV () Int)
+(assert ( and ( >= global_invc1_0 ( - 1 ) ) ( <= global_invc1_0 1 ) ( and ( >= lam0n0 0 ) ( <= 0 lam0n2 ) ( < lam0n2 1 ) ( and ( = ( * ( - 1 ) lam0n0 ) ( + global_invc1_1 ( * ( - 1 ) lam0n2 ) ) ) ( = ( * lam0n1 1 ) 0 ) ( = ( * lam0n1 ( - 1 ) ) global_invc1_0 ) ) ) ( and ( >= lam1n0 0 ) ( >= lam1n1 0 ) ( >= lam1n3 0 ) ( <= 0 lam1n4 ) ( < lam1n4 1 ) ( and ( = ( + ( * ( - 1 ) lam1n0 ) ( * lam1n1 ( - 999 ) ) ( * lam1n2 1000 ) ( * lam1n3 global_invc1_1 ) ) ( + global_invc1_1 ( * ( - 1 ) lam1n4 ) ) ) ( = ( + ( * lam1n1 ( - 1 ) ) ( * lam1n2 1 ) ( * lam1n3 global_invc1_0 ) ) 0 ) ( = ( * lam1n2 ( - 1 ) ) global_invc1_0 ) ) ) ( >= term_invc1_0 ( - 1 ) ) ( <= term_invc1_0 1 ) ( and ( >= lam2n0 0 ) ( >= lam2n1 0 ) ( >= lam2n3 0 ) ( >= lam2n4 0 ) ( >= lam2n5 0 ) ( >= lam2n6 0 ) ( >= lam2n7 0 ) ( >= lam2n8 0 ) ( >= lam2n9 0 ) ( >= lam2n10 0 ) ( >= lam2n11 0 ) ( >= lam2n12 0 ) ( <= 0 lam2n13 ) ( < lam2n13 1 ) ( and ( = ( + ( * ( - 1 ) lam2n0 ) ( * lam2n1 ( - 999 ) ) ( * lam2n2 1000 ) ( * lam2n3 50001 ) ( * lam2n4 ( - 1 ) ) ( * lam2n5 1 ) ( * lam2n6 2 ) ( * lam2n7 3 ) ( * lam2n8 55 ) ( * lam2n9 58 ) ( * lam2n10 61 ) ( * lam2n11 62 ) ( * lam2n12 global_invc1_1 ) ) ( + term_invc1_1 ( * ( - 1 ) lam2n13 ) ) ) ( = ( + ( * lam2n1 ( - 1 ) ) ( * lam2n2 1 ) ( * lam2n3 ( - 1 ) ) ( * lam2n4 ( - 1 ) ) ( * lam2n5 ( - 1 ) ) ( * lam2n6 ( - 1 ) ) ( * lam2n7 ( - 1 ) ) ( * lam2n8 ( - 1 ) ) ( * lam2n9 ( - 1 ) ) ( * lam2n10 ( - 1 ) ) ( * lam2n11 ( - 1 ) ) ( * lam2n12 global_invc1_0 ) ) 0 ) ( = ( * lam2n2 ( - 1 ) ) term_invc1_0 ) ) ) ( = non_inc1_L ( and ( >= lam3n0 0 ) ( >= lam3n1 0 ) ( >= lam3n3 0 ) ( >= lam3n4 0 ) ( >= lam3n5 0 ) ( >= lam3n6 0 ) ( >= lam3n7 0 ) ( >= lam3n8 0 ) ( >= lam3n9 0 ) ( >= lam3n10 0 ) ( >= lam3n11 0 ) ( >= lam3n12 0 ) ( >= lam3n13 0 ) ( <= 0 lam3n15 ) ( < lam3n15 1 ) ( <= lam3n14 1 ) ( >= lam3n14 0 ) ( and ( > ( + ( * ( - 1 ) lam3n0 ) ( * lam3n1 ( - 999 ) ) ( * lam3n2 1000 ) ( * lam3n3 50001 ) ( * lam3n4 ( - 1 ) ) ( * lam3n5 1 ) ( * lam3n6 2 ) ( * lam3n7 3 ) ( * lam3n8 55 ) ( * lam3n9 58 ) ( * lam3n10 61 ) ( * lam3n11 62 ) ( * lam3n12 global_invc1_1 ) ( * lam3n13 term_invc1_1 ) ( * lam3n14 ( + 1 ( * ( - 1 ) lam3n15 ) ) ) ) 0 ) ( = ( + ( * lam3n1 ( - 1 ) ) ( * lam3n2 1 ) ( * lam3n3 ( - 1 ) ) ( * lam3n4 ( - 1 ) ) ( * lam3n5 ( - 1 ) ) ( * lam3n6 ( - 1 ) ) ( * lam3n7 ( - 1 ) ) ( * lam3n8 ( - 1 ) ) ( * lam3n9 ( - 1 ) ) ( * lam3n10 ( - 1 ) ) ( * lam3n11 ( - 1 ) ) ( * lam3n12 global_invc1_0 ) ( * lam3n13 term_invc1_0 ) ( * lam3n14 rfc0 ) ) 0 ) ( = ( + ( * lam3n2 ( - 1 ) ) ( * lam3n14 ( * ( - 1 ) rfc0 ) ) ) 0 ) ) ) ) ( = disabled1_L ( and ( = lam3n14 0 ) non_inc1_L ) ) ( = bounded1_L ( and ( >= lam4n0 0 ) ( >= lam4n1 0 ) ( >= lam4n3 0 ) ( >= lam4n4 0 ) ( >= lam4n5 0 ) ( >= lam4n6 0 ) ( >= lam4n7 0 ) ( >= lam4n8 0 ) ( >= lam4n9 0 ) ( >= lam4n10 0 ) ( >= lam4n11 0 ) ( >= lam4n12 0 ) ( >= lam4n13 0 ) ( <= 0 lam4n14 ) ( < lam4n14 1 ) ( and ( = ( + ( * ( - 1 ) lam4n0 ) ( * lam4n1 ( - 999 ) ) ( * lam4n2 1000 ) ( * lam4n3 50001 ) ( * lam4n4 ( - 1 ) ) ( * lam4n5 1 ) ( * lam4n6 2 ) ( * lam4n7 3 ) ( * lam4n8 55 ) ( * lam4n9 58 ) ( * lam4n10 61 ) ( * lam4n11 62 ) ( * lam4n12 global_invc1_1 ) ( * lam4n13 term_invc1_1 ) ) ( + ( * ( - 1 ) rfc1 ) ( * ( - 1 ) lam4n14 ) ) ) ( = ( + ( * lam4n1 ( - 1 ) ) ( * lam4n2 1 ) ( * lam4n3 ( - 1 ) ) ( * lam4n4 ( - 1 ) ) ( * lam4n5 ( - 1 ) ) ( * lam4n6 ( - 1 ) ) ( * lam4n7 ( - 1 ) ) ( * lam4n8 ( - 1 ) ) ( * lam4n9 ( - 1 ) ) ( * lam4n10 ( - 1 ) ) ( * lam4n11 ( - 1 ) ) ( * lam4n12 global_invc1_0 ) ( * lam4n13 term_invc1_0 ) ) ( * ( - 1 ) rfc0 ) ) ( = ( * lam4n2 ( - 1 ) ) 0 ) ) ) ) ( = dec1_L ( and ( >= lam5n0 0 ) ( >= lam5n1 0 ) ( >= lam5n3 0 ) ( >= lam5n4 0 ) ( >= lam5n5 0 ) ( >= lam5n6 0 ) ( >= lam5n7 0 ) ( >= lam5n8 0 ) ( >= lam5n9 0 ) ( >= lam5n10 0 ) ( >= lam5n11 0 ) ( >= lam5n12 0 ) ( >= lam5n13 0 ) ( <= 0 lam5n14 ) ( < lam5n14 1 ) ( and ( = ( + ( * ( - 1 ) lam5n0 ) ( * lam5n1 ( - 999 ) ) ( * lam5n2 1000 ) ( * lam5n3 50001 ) ( * lam5n4 ( - 1 ) ) ( * lam5n5 1 ) ( * lam5n6 2 ) ( * lam5n7 3 ) ( * lam5n8 55 ) ( * lam5n9 58 ) ( * lam5n10 61 ) ( * lam5n11 62 ) ( * lam5n12 global_invc1_1 ) ( * lam5n13 term_invc1_1 ) ) ( + 1 ( * ( - 1 ) lam5n14 ) ) ) ( = ( + ( * lam5n1 ( - 1 ) ) ( * lam5n2 1 ) ( * lam5n3 ( - 1 ) ) ( * lam5n4 ( - 1 ) ) ( * lam5n5 ( - 1 ) ) ( * lam5n6 ( - 1 ) ) ( * lam5n7 ( - 1 ) ) ( * lam5n8 ( - 1 ) ) ( * lam5n9 ( - 1 ) ) ( * lam5n10 ( - 1 ) ) ( * lam5n11 ( - 1 ) ) ( * lam5n12 global_invc1_0 ) ( * lam5n13 term_invc1_0 ) ) ( * ( - 1 ) rfc0 ) ) ( = ( * lam5n2 ( - 1 ) ) rfc0 ) ) ) ) ( = bnd_and_dec1_L ( and bounded1_L dec1_L ) ) ( = GLOBAL_NT_1 ( not ( = global_invc1_0 0 ) ) ) ( or ( not ( <= ( + global_invc1_1 ( * global_invc1_0 global_V0_1 ) ) 0 ) ) ( = global_invc1_0 0 ) ) ( = TERM_NT_1 ( not ( = term_invc1_0 0 ) ) ) ( or ( and ( not ( <= ( + term_invc1_1 ( * term_invc1_0 term_V0_1 ) ) 0 ) ) ( <= ( + ( * ( - 1 ) term_V0_1 ) ( - 1 ) ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 1 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 2 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 3 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 55 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 58 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 61 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 62 ) 0 ) ) ( = term_invc1_0 0 ) ) ( = ALL_NON_INC_0 non_inc1_L ) ( = DIS_OR_ALL_NON_INC_0 ( or disabled1_L ALL_NON_INC_0 ) ) ( = SOME_BND_AND_DEC_0 bnd_and_dec1_L ) ( or ( not ALL_NON_INC_0 ) ( and ( >= rfc0 ( - 2 ) ) ( <= rfc0 2 ) ( not ( = rfc0 0 ) ) ( >= rfc1 0 ) ( or SOME_BND_AND_DEC_0 ( or ( and ( <= ( + ( * rfc0 V0_NIV ) 1 ) ( * rfc0 V1_NIV ) ) ( >= ( * ( - 1 ) V0_NIV ) ( * ( - 1 ) V1_NIV ) ) ) ( = rfc0 0 ) ) ) ) ) ( or GLOBAL_NT_1 TERM_NT_1 ALL_NON_INC_0 ) ))
+(check-sat)
+(exit)