diff options
Diffstat (limited to 'test/regress/regress0/uflia')
28 files changed, 155 insertions, 1262 deletions
diff --git a/test/regress/regress0/uflia/diseqprop.01.smt b/test/regress/regress0/uflia/diseqprop.01.smt deleted file mode 100644 index 93544639e..000000000 --- a/test/regress/regress0/uflia/diseqprop.01.smt +++ /dev/null @@ -1,19 +0,0 @@ -(benchmark test -:logic QF_UFLIA -:extrafuns ((f Int Int)) -:extrafuns ((x1 Int)) -:extrafuns ((y1 Int)) -:extrafuns ((x2 Int)) -:extrafuns ((y2 Int)) - -:extrafuns ((a Int)) -:extrafuns ((b Int)) - -:assumption (not (= x2 y2)) -:assumption (= x1 x2) -:assumption (= y1 y2) - -:assumption (= (f x1) (f y1)) - -:formula true -) diff --git a/test/regress/regress0/uflia/diseqprop.01.smtv1.smt2 b/test/regress/regress0/uflia/diseqprop.01.smtv1.smt2 new file mode 100644 index 000000000..5432077c0 --- /dev/null +++ b/test/regress/regress0/uflia/diseqprop.01.smtv1.smt2 @@ -0,0 +1,14 @@ +(set-option :incremental false) +(set-logic QF_UFLIA) +(declare-fun f (Int) Int) +(declare-fun x1 () Int) +(declare-fun y1 () Int) +(declare-fun x2 () Int) +(declare-fun y2 () Int) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (not (= x2 y2))) +(assert (= x1 x2)) +(assert (= y1 y2)) +(assert (= (f x1) (f y1))) +(check-sat-assuming ( true )) diff --git a/test/regress/regress0/uflia/diseqprop.02.smt b/test/regress/regress0/uflia/diseqprop.02.smt deleted file mode 100644 index 3d34c6e80..000000000 --- a/test/regress/regress0/uflia/diseqprop.02.smt +++ /dev/null @@ -1,20 +0,0 @@ -(benchmark test -:logic QF_UFLIA -:extrafuns ((f Int Int)) -:extrafuns ((x1 Int)) -:extrafuns ((y1 Int)) -:extrafuns ((x2 Int)) -:extrafuns ((y2 Int)) - -:extrafuns ((a Int)) -:extrafuns ((b Int)) - -:assumption (= x1 x2) -:assumption (= y1 y2) - -:assumption (= (f x1) (f y1)) - -:assumption (not (= x2 y2)) - -:formula true -) diff --git a/test/regress/regress0/uflia/diseqprop.02.smtv1.smt2 b/test/regress/regress0/uflia/diseqprop.02.smtv1.smt2 new file mode 100644 index 000000000..e146bd7fd --- /dev/null +++ b/test/regress/regress0/uflia/diseqprop.02.smtv1.smt2 @@ -0,0 +1,14 @@ +(set-option :incremental false) +(set-logic QF_UFLIA) +(declare-fun f (Int) Int) +(declare-fun x1 () Int) +(declare-fun y1 () Int) +(declare-fun x2 () Int) +(declare-fun y2 () Int) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (= x1 x2)) +(assert (= y1 y2)) +(assert (= (f x1) (f y1))) +(assert (not (= x2 y2))) +(check-sat-assuming ( true )) diff --git a/test/regress/regress0/uflia/diseqprop.03.smt b/test/regress/regress0/uflia/diseqprop.03.smt deleted file mode 100644 index 80c4eb822..000000000 --- a/test/regress/regress0/uflia/diseqprop.03.smt +++ /dev/null @@ -1,20 +0,0 @@ -(benchmark test -:logic QF_UFLIA -:extrafuns ((f Int Int)) -:extrafuns ((x1 Int)) -:extrafuns ((y1 Int)) -:extrafuns ((x2 Int)) -:extrafuns ((y2 Int)) - -:extrafuns ((a Int)) -:extrafuns ((b Int)) - -:assumption (= x1 x2) - -:assumption (= (f x1) (f y1)) - -:assumption (not (= x2 y2)) -:assumption (= y1 y2) - -:formula true -) diff --git a/test/regress/regress0/uflia/diseqprop.03.smtv1.smt2 b/test/regress/regress0/uflia/diseqprop.03.smtv1.smt2 new file mode 100644 index 000000000..3acee371b --- /dev/null +++ b/test/regress/regress0/uflia/diseqprop.03.smtv1.smt2 @@ -0,0 +1,14 @@ +(set-option :incremental false) +(set-logic QF_UFLIA) +(declare-fun f (Int) Int) +(declare-fun x1 () Int) +(declare-fun y1 () Int) +(declare-fun x2 () Int) +(declare-fun y2 () Int) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (= x1 x2)) +(assert (= (f x1) (f y1))) +(assert (not (= x2 y2))) +(assert (= y1 y2)) +(check-sat-assuming ( true )) diff --git a/test/regress/regress0/uflia/diseqprop.04.smt b/test/regress/regress0/uflia/diseqprop.04.smt deleted file mode 100644 index f07a0f373..000000000 --- a/test/regress/regress0/uflia/diseqprop.04.smt +++ /dev/null @@ -1,20 +0,0 @@ -(benchmark test -:logic QF_UFLIA -:extrafuns ((f Int Int)) -:extrafuns ((x1 Int)) -:extrafuns ((y1 Int)) -:extrafuns ((x2 Int)) -:extrafuns ((y2 Int)) - -:extrafuns ((a Int)) -:extrafuns ((b Int)) - -:assumption (= y1 y2) - -:assumption (= (f x1) (f y1)) - -:assumption (not (= x2 y2)) -:assumption (= x1 x2) - -:formula true -) diff --git a/test/regress/regress0/uflia/diseqprop.04.smtv1.smt2 b/test/regress/regress0/uflia/diseqprop.04.smtv1.smt2 new file mode 100644 index 000000000..a1fec8795 --- /dev/null +++ b/test/regress/regress0/uflia/diseqprop.04.smtv1.smt2 @@ -0,0 +1,14 @@ +(set-option :incremental false) +(set-logic QF_UFLIA) +(declare-fun f (Int) Int) +(declare-fun x1 () Int) +(declare-fun y1 () Int) +(declare-fun x2 () Int) +(declare-fun y2 () Int) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (= y1 y2)) +(assert (= (f x1) (f y1))) +(assert (not (= x2 y2))) +(assert (= x1 x2)) +(check-sat-assuming ( true )) diff --git a/test/regress/regress0/uflia/diseqprop.05.smt b/test/regress/regress0/uflia/diseqprop.05.smt deleted file mode 100644 index 5510e57c9..000000000 --- a/test/regress/regress0/uflia/diseqprop.05.smt +++ /dev/null @@ -1,20 +0,0 @@ -(benchmark test -:logic QF_UFLIA -:extrafuns ((f Int Int)) -:extrafuns ((x1 Int)) -:extrafuns ((y1 Int)) -:extrafuns ((x2 Int)) -:extrafuns ((y2 Int)) - -:extrafuns ((a Int)) -:extrafuns ((b Int)) - -:assumption (= x1 x2) -:assumption (= y1 y2) - -:assumption (= (f x1) (f y1)) -:assumption (= x2 1) -:assumption (= y2 2) - -:formula true -) diff --git a/test/regress/regress0/uflia/diseqprop.05.smtv1.smt2 b/test/regress/regress0/uflia/diseqprop.05.smtv1.smt2 new file mode 100644 index 000000000..dc18a4560 --- /dev/null +++ b/test/regress/regress0/uflia/diseqprop.05.smtv1.smt2 @@ -0,0 +1,15 @@ +(set-option :incremental false) +(set-logic QF_UFLIA) +(declare-fun f (Int) Int) +(declare-fun x1 () Int) +(declare-fun y1 () Int) +(declare-fun x2 () Int) +(declare-fun y2 () Int) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (= x1 x2)) +(assert (= y1 y2)) +(assert (= (f x1) (f y1))) +(assert (= x2 1)) +(assert (= y2 2)) +(check-sat-assuming ( true )) diff --git a/test/regress/regress0/uflia/diseqprop.06.smt b/test/regress/regress0/uflia/diseqprop.06.smt deleted file mode 100644 index b27a5a73c..000000000 --- a/test/regress/regress0/uflia/diseqprop.06.smt +++ /dev/null @@ -1,21 +0,0 @@ -(benchmark test -:logic QF_UFLIA -:extrafuns ((f Int Int)) -:extrafuns ((x1 Int)) -:extrafuns ((y1 Int)) -:extrafuns ((x2 Int)) -:extrafuns ((y2 Int)) - -:extrafuns ((a Int)) -:extrafuns ((b Int)) - -:assumption (= x1 x2) -:assumption (= y1 y2) - -:assumption (= x2 1) -:assumption (= y2 2) - -:assumption (= (f x1) (f y1)) - -:formula true -) diff --git a/test/regress/regress0/uflia/diseqprop.06.smtv1.smt2 b/test/regress/regress0/uflia/diseqprop.06.smtv1.smt2 new file mode 100644 index 000000000..0e411d752 --- /dev/null +++ b/test/regress/regress0/uflia/diseqprop.06.smtv1.smt2 @@ -0,0 +1,15 @@ +(set-option :incremental false) +(set-logic QF_UFLIA) +(declare-fun f (Int) Int) +(declare-fun x1 () Int) +(declare-fun y1 () Int) +(declare-fun x2 () Int) +(declare-fun y2 () Int) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (= x1 x2)) +(assert (= y1 y2)) +(assert (= x2 1)) +(assert (= y2 2)) +(assert (= (f x1) (f y1))) +(check-sat-assuming ( true )) diff --git a/test/regress/regress0/uflia/error0.delta01.smt b/test/regress/regress0/uflia/error0.delta01.smt deleted file mode 100644 index cc205063c..000000000 --- a/test/regress/regress0/uflia/error0.delta01.smt +++ /dev/null @@ -1,78 +0,0 @@ -(benchmark B_ -:logic QF_UFLIA -:extrafuns ((format Int Int)) -:extrafuns ((arg1 Int)) -:extrafuns ((fmt1 Int)) -:extrafuns ((s_count Int Int)) -:extrafuns ((fmt0 Int)) -:extrafuns ((x_count Int Int)) -:status sat -:formula -(flet ($n1 true) -(let (?n2 1) -(let (?n3 (~ ?n2)) -(let (?n4 (* ?n3 fmt1)) -(let (?n5 (+ ?n4 fmt0)) -(let (?n6 8) -(let (?n7 (~ ?n6)) -(flet ($n8 (>= ?n5 ?n7)) -(let (?n9 6) -(let (?n10 (x_count ?n9)) -(let (?n11 7) -(let (?n12 (x_count ?n11)) -(let (?n13 (* ?n3 ?n12)) -(let (?n14 (+ ?n10 ?n13)) -(let (?n15 0) -(flet ($n16 (>= ?n14 ?n15)) -(flet ($n17 (>= fmt1 ?n11)) -(flet ($n18 (<= arg1 ?n9)) -(let (?n19 2) -(let (?n20 (~ ?n19)) -(let (?n21 (* ?n3 fmt0)) -(let (?n22 (+ fmt1 ?n20 ?n21)) -(let (?n23 (s_count ?n22)) -(let (?n24 5) -(let (?n25 (s_count ?n24)) -(let (?n26 (* ?n3 ?n25)) -(let (?n27 (+ ?n23 ?n26)) -(flet ($n28 (= ?n15 ?n27)) -(flet ($n29 (not $n28)) -(let (?n30 (~ ?n11)) -(flet ($n31 (<= ?n5 ?n30)) -(flet ($n32 false) -(let (?n33 (+ arg1 ?n21)) -(flet ($n34 (<= ?n33 ?n2)) -(let (?n35 (+ ?n4 arg1)) -(flet ($n36 (<= ?n35 ?n15)) -(flet ($n37 (or $n32 $n32 $n34 $n36)) -(let (?n38 (x_count ?n2)) -(flet ($n39 (>= ?n38 ?n15)) -(let (?n40 (format ?n11)) -(flet ($n41 (<= ?n40 ?n15)) -(let (?n42 (x_count ?n22)) -(let (?n43 (+ ?n13 ?n42)) -(flet ($n44 (= ?n15 ?n43)) -(let (?n45 (s_count ?n9)) -(let (?n46 (* ?n3 ?n45)) -(let (?n47 (+ ?n23 ?n46)) -(flet ($n48 (= ?n15 ?n47)) -(flet ($n49 (or $n32 $n32 $n32 $n32 $n32 $n39 $n44 $n48)) -(let (?n50 (+ ?n2 fmt1)) -(let (?n51 (format ?n50)) -(flet ($n52 (>= ?n51 ?n15)) -(let (?n53 4) -(let (?n54 (format ?n53)) -(flet ($n55 (>= ?n54 ?n15)) -(let (?n56 9) -(let (?n57 (format ?n56)) -(flet ($n58 (<= ?n57 ?n15)) -(let (?n59 (format fmt1)) -(flet ($n60 (>= ?n59 ?n15)) -(let (?n61 12) -(let (?n62 (format ?n61)) -(flet ($n63 (>= ?n62 ?n15)) -(let (?n64 (format arg1)) -(flet ($n65 (= ?n15 ?n64)) -(flet ($n66 (and $n1 $n8 $n16 $n17 $n18 $n29 $n31 $n37 $n39 $n41 $n49 $n52 $n55 $n58 $n60 $n63 $n65)) -$n66 -))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/error0.delta01.smtv1.smt2 b/test/regress/regress0/uflia/error0.delta01.smtv1.smt2 new file mode 100644 index 000000000..bc2d0166c --- /dev/null +++ b/test/regress/regress0/uflia/error0.delta01.smtv1.smt2 @@ -0,0 +1,10 @@ +(set-option :incremental false) +(set-info :status sat) +(set-logic QF_UFLIA) +(declare-fun format (Int) Int) +(declare-fun arg1 () Int) +(declare-fun fmt1 () Int) +(declare-fun s_count (Int) Int) +(declare-fun fmt0 () Int) +(declare-fun x_count (Int) Int) +(check-sat-assuming ( (let ((_let_0 (* (- 1) fmt1))) (let ((_let_1 (+ _let_0 fmt0))) (let ((_let_2 (* (- 1) (x_count 7)))) (let ((_let_3 (+ fmt1 (- 2) (* (- 1) fmt0)))) (let ((_let_4 (s_count _let_3))) (let ((_let_5 (>= (x_count 1) 0))) (and true (>= _let_1 (- 8)) (>= (+ (x_count 6) _let_2) 0) (>= fmt1 7) (<= arg1 6) (not (= 0 (+ _let_4 (* (- 1) (s_count 5))))) (<= _let_1 (- 7)) (or false false (<= (+ arg1 (* (- 1) fmt0)) 1) (<= (+ _let_0 arg1) 0)) _let_5 (<= (format 7) 0) (or false false false false false _let_5 (= 0 (+ _let_2 (x_count _let_3))) (= 0 (+ _let_4 (* (- 1) (s_count 6))))) (>= (format (+ 1 fmt1)) 0) (>= (format 4) 0) (<= (format 9) 0) (>= (format fmt1) 0) (>= (format 12) 0) (= 0 (format arg1))))))))) )) diff --git a/test/regress/regress0/uflia/error1.smt b/test/regress/regress0/uflia/error1.smt deleted file mode 100644 index 7afffaa88..000000000 --- a/test/regress/regress0/uflia/error1.smt +++ /dev/null @@ -1,701 +0,0 @@ -(benchmark fuzzsmt -:logic QF_UFLIA -:status sat -:extrafuns ((f0 Int Int Int Int)) -:extrafuns ((f1 Int Int)) -:extrapreds ((p0 Int Int)) -:extrafuns ((v0 Int)) -:extrafuns ((v1 Int)) -:extrafuns ((v2 Int)) -:formula -(let (?e3 1) -(let (?e4 2) -(let (?e5 (f1 v1)) -(let (?e6 (+ v2 v2)) -(let (?e7 (ite (p0 ?e6 v1) 1 0)) -(let (?e8 (ite (p0 ?e5 v1) 1 0)) -(let (?e9 (+ ?e6 ?e8)) -(let (?e10 (ite (p0 v1 ?e6) 1 0)) -(let (?e11 (ite (p0 v2 ?e8) 1 0)) -(let (?e12 (* (~ ?e4) ?e6)) -(let (?e13 (+ v1 ?e5)) -(let (?e14 (* ?e4 ?e12)) -(let (?e15 (f0 v2 ?e5 v0)) -(let (?e16 (ite (p0 ?e5 ?e6) 1 0)) -(let (?e17 (+ ?e7 ?e16)) -(let (?e18 (+ ?e10 ?e12)) -(let (?e19 (- ?e13 ?e12)) -(let (?e20 (* ?e19 (~ ?e4))) -(let (?e21 (+ ?e13 ?e18)) -(let (?e22 (f0 ?e5 ?e17 ?e5)) -(let (?e23 (* ?e17 ?e4)) -(let (?e24 (ite (p0 ?e9 ?e19) 1 0)) -(let (?e25 (~ ?e6)) -(let (?e26 (f1 ?e6)) -(let (?e27 (* ?e25 (~ ?e3))) -(flet ($e28 (< ?e7 ?e6)) -(flet ($e29 (> ?e12 ?e10)) -(flet ($e30 (distinct ?e7 ?e9)) -(flet ($e31 (<= v2 v2)) -(flet ($e32 (>= ?e6 ?e27)) -(flet ($e33 (distinct ?e11 ?e20)) -(flet ($e34 (> ?e25 ?e23)) -(flet ($e35 (< ?e7 ?e22)) -(flet ($e36 (>= ?e24 ?e10)) -(flet ($e37 (>= ?e24 ?e23)) -(flet ($e38 (distinct ?e5 ?e25)) -(flet ($e39 (= ?e16 ?e27)) -(flet ($e40 (> ?e21 ?e16)) -(flet ($e41 (> ?e7 ?e12)) -(flet ($e42 (distinct ?e22 ?e22)) -(flet ($e43 (= v2 ?e16)) -(flet ($e44 (>= ?e23 ?e7)) -(flet ($e45 (= ?e12 ?e8)) -(flet ($e46 (<= ?e13 ?e12)) -(flet ($e47 (< ?e12 ?e24)) -(flet ($e48 (< ?e13 ?e6)) -(flet ($e49 (> ?e15 ?e19)) -(flet ($e50 (> ?e25 ?e18)) -(flet ($e51 (>= ?e15 ?e7)) -(flet ($e52 (distinct ?e8 ?e20)) -(flet ($e53 (= ?e18 ?e5)) -(flet ($e54 (> ?e13 ?e15)) -(flet ($e55 (= ?e14 ?e16)) -(flet ($e56 (>= v0 ?e21)) -(flet ($e57 (= v1 ?e10)) -(flet ($e58 (distinct ?e26 ?e22)) -(flet ($e59 (> ?e18 ?e5)) -(flet ($e60 (< ?e11 ?e10)) -(flet ($e61 (>= ?e8 ?e11)) -(flet ($e62 (distinct ?e23 ?e21)) -(flet ($e63 (p0 v1 ?e20)) -(flet ($e64 (< ?e8 ?e11)) -(flet ($e65 (<= ?e26 ?e12)) -(flet ($e66 (= ?e21 ?e6)) -(flet ($e67 (distinct ?e21 ?e21)) -(flet ($e68 (>= v1 ?e17)) -(let (?e69 (ite $e59 ?e16 ?e12)) -(let (?e70 (ite $e47 ?e9 ?e19)) -(let (?e71 (ite $e64 ?e9 ?e25)) -(let (?e72 (ite $e63 v2 ?e25)) -(let (?e73 (ite $e31 ?e22 ?e15)) -(let (?e74 (ite $e66 ?e23 ?e20)) -(let (?e75 (ite $e57 ?e15 ?e9)) -(let (?e76 (ite $e39 ?e21 ?e75)) -(let (?e77 (ite $e62 v0 ?e11)) -(let (?e78 (ite $e50 ?e17 ?e71)) -(let (?e79 (ite $e38 ?e6 v0)) -(let (?e80 (ite $e62 ?e18 v0)) -(let (?e81 (ite $e29 ?e70 ?e13)) -(let (?e82 (ite $e54 ?e19 ?e20)) -(let (?e83 (ite $e57 ?e19 ?e77)) -(let (?e84 (ite $e41 ?e79 v2)) -(let (?e85 (ite $e56 ?e84 v2)) -(let (?e86 (ite $e47 ?e7 ?e15)) -(let (?e87 (ite $e49 ?e27 ?e27)) -(let (?e88 (ite $e45 ?e14 ?e16)) -(let (?e89 (ite $e42 ?e26 ?e5)) -(let (?e90 (ite $e51 ?e10 ?e12)) -(let (?e91 (ite $e46 ?e26 ?e16)) -(let (?e92 (ite $e35 ?e24 v1)) -(let (?e93 (ite $e32 ?e8 ?e91)) -(let (?e94 (ite $e30 ?e80 ?e15)) -(let (?e95 (ite $e56 ?e75 ?e27)) -(let (?e96 (ite $e64 ?e79 ?e19)) -(let (?e97 (ite $e44 ?e77 ?e84)) -(let (?e98 (ite $e62 ?e25 ?e71)) -(let (?e99 (ite $e65 ?e91 ?e21)) -(let (?e100 (ite $e33 ?e97 ?e14)) -(let (?e101 (ite $e45 ?e90 ?e7)) -(let (?e102 (ite $e41 ?e78 ?e89)) -(let (?e103 (ite $e36 ?e7 ?e81)) -(let (?e104 (ite $e48 ?e74 ?e16)) -(let (?e105 (ite $e31 ?e24 ?e81)) -(let (?e106 (ite $e40 ?e83 ?e71)) -(let (?e107 (ite $e67 ?e11 ?e10)) -(let (?e108 (ite $e52 ?e104 ?e76)) -(let (?e109 (ite $e55 ?e14 ?e14)) -(let (?e110 (ite $e61 ?e102 ?e80)) -(let (?e111 (ite $e34 ?e74 v2)) -(let (?e112 (ite $e54 ?e21 ?e106)) -(let (?e113 (ite $e28 ?e93 ?e20)) -(let (?e114 (ite $e37 ?e8 ?e83)) -(let (?e115 (ite $e55 ?e113 ?e89)) -(let (?e116 (ite $e58 ?e7 ?e25)) -(let (?e117 (ite $e60 ?e7 ?e75)) -(let (?e118 (ite $e43 ?e75 ?e16)) -(let (?e119 (ite $e53 ?e74 ?e26)) -(let (?e120 (ite $e68 ?e76 ?e25)) -(flet ($e121 (< ?e90 ?e9)) -(flet ($e122 (distinct ?e99 v0)) -(flet ($e123 (= ?e116 ?e23)) -(flet ($e124 (= ?e86 ?e99)) -(flet ($e125 (>= ?e78 ?e18)) -(flet ($e126 (> ?e99 ?e75)) -(flet ($e127 (<= ?e84 ?e107)) -(flet ($e128 (>= ?e9 ?e69)) -(flet ($e129 (= ?e95 ?e79)) -(flet ($e130 (p0 ?e103 ?e16)) -(flet ($e131 (<= ?e83 ?e104)) -(flet ($e132 (p0 ?e119 ?e97)) -(flet ($e133 (p0 ?e96 ?e89)) -(flet ($e134 (<= ?e100 ?e21)) -(flet ($e135 (= ?e102 ?e18)) -(flet ($e136 (<= ?e81 ?e16)) -(flet ($e137 (distinct ?e70 ?e94)) -(flet ($e138 (= ?e114 ?e112)) -(flet ($e139 (= ?e107 ?e89)) -(flet ($e140 (p0 ?e110 v2)) -(flet ($e141 (< ?e21 ?e114)) -(flet ($e142 (p0 ?e20 v2)) -(flet ($e143 (< ?e100 ?e94)) -(flet ($e144 (distinct ?e94 ?e26)) -(flet ($e145 (= ?e109 ?e88)) -(flet ($e146 (= ?e16 ?e100)) -(flet ($e147 (= ?e99 ?e87)) -(flet ($e148 (<= ?e87 ?e86)) -(flet ($e149 (p0 ?e73 ?e96)) -(flet ($e150 (> ?e12 ?e94)) -(flet ($e151 (distinct ?e95 ?e71)) -(flet ($e152 (distinct ?e19 ?e101)) -(flet ($e153 (p0 ?e84 ?e96)) -(flet ($e154 (= ?e99 ?e111)) -(flet ($e155 (p0 ?e14 ?e118)) -(flet ($e156 (<= ?e70 ?e25)) -(flet ($e157 (= ?e19 ?e98)) -(flet ($e158 (< ?e99 ?e90)) -(flet ($e159 (>= ?e14 ?e15)) -(flet ($e160 (<= v2 ?e120)) -(flet ($e161 (<= ?e21 ?e75)) -(flet ($e162 (< ?e114 ?e6)) -(flet ($e163 (> ?e99 ?e116)) -(flet ($e164 (<= ?e89 ?e11)) -(flet ($e165 (distinct ?e9 ?e10)) -(flet ($e166 (> ?e27 ?e97)) -(flet ($e167 (< ?e119 ?e10)) -(flet ($e168 (< ?e69 ?e79)) -(flet ($e169 (<= ?e22 ?e7)) -(flet ($e170 (= ?e117 ?e17)) -(flet ($e171 (>= ?e72 ?e16)) -(flet ($e172 (>= ?e12 ?e114)) -(flet ($e173 (distinct ?e119 ?e27)) -(flet ($e174 (<= ?e72 ?e119)) -(flet ($e175 (= ?e119 ?e118)) -(flet ($e176 (distinct ?e80 ?e73)) -(flet ($e177 (> ?e10 ?e18)) -(flet ($e178 (> ?e115 ?e15)) -(flet ($e179 (= ?e13 ?e72)) -(flet ($e180 (>= ?e110 ?e111)) -(flet ($e181 (< v0 ?e87)) -(flet ($e182 (< ?e72 ?e70)) -(flet ($e183 (<= ?e13 ?e9)) -(flet ($e184 (>= ?e7 ?e20)) -(flet ($e185 (<= ?e77 ?e23)) -(flet ($e186 (< ?e105 ?e102)) -(flet ($e187 (<= ?e78 ?e109)) -(flet ($e188 (distinct ?e89 ?e97)) -(flet ($e189 (p0 ?e118 ?e97)) -(flet ($e190 (> ?e81 ?e111)) -(flet ($e191 (> ?e14 ?e78)) -(flet ($e192 (< ?e101 ?e97)) -(flet ($e193 (distinct ?e12 ?e16)) -(flet ($e194 (< ?e113 ?e92)) -(flet ($e195 (>= ?e100 ?e87)) -(flet ($e196 (>= ?e103 ?e12)) -(flet ($e197 (p0 ?e116 ?e13)) -(flet ($e198 (>= ?e85 ?e13)) -(flet ($e199 (p0 ?e107 ?e120)) -(flet ($e200 (> ?e96 ?e74)) -(flet ($e201 (<= ?e113 ?e113)) -(flet ($e202 (>= ?e16 ?e103)) -(flet ($e203 (>= ?e72 ?e11)) -(flet ($e204 (> ?e27 ?e25)) -(flet ($e205 (distinct ?e25 ?e15)) -(flet ($e206 (distinct v1 ?e85)) -(flet ($e207 (p0 ?e95 ?e75)) -(flet ($e208 (< ?e92 ?e84)) -(flet ($e209 (< ?e91 ?e115)) -(flet ($e210 (distinct ?e13 ?e75)) -(flet ($e211 (= ?e91 ?e69)) -(flet ($e212 (p0 ?e13 ?e23)) -(flet ($e213 (>= ?e96 ?e100)) -(flet ($e214 (>= ?e72 ?e111)) -(flet ($e215 (p0 ?e97 ?e112)) -(flet ($e216 (>= ?e78 ?e98)) -(flet ($e217 (= ?e120 ?e101)) -(flet ($e218 (<= ?e72 ?e71)) -(flet ($e219 (p0 ?e90 ?e103)) -(flet ($e220 (< ?e117 ?e113)) -(flet ($e221 (>= ?e118 ?e84)) -(flet ($e222 (> ?e11 ?e104)) -(flet ($e223 (< ?e77 ?e111)) -(flet ($e224 (<= ?e21 ?e7)) -(flet ($e225 (>= ?e16 ?e74)) -(flet ($e226 (<= ?e91 ?e74)) -(flet ($e227 (p0 v2 ?e70)) -(flet ($e228 (p0 ?e101 ?e83)) -(flet ($e229 (>= ?e10 ?e8)) -(flet ($e230 (> ?e110 ?e72)) -(flet ($e231 (< ?e84 ?e20)) -(flet ($e232 (p0 ?e79 ?e26)) -(flet ($e233 (= ?e113 ?e81)) -(flet ($e234 (p0 ?e14 ?e90)) -(flet ($e235 (distinct ?e96 ?e15)) -(flet ($e236 (distinct ?e96 ?e7)) -(flet ($e237 (p0 ?e87 ?e104)) -(flet ($e238 (= ?e110 ?e71)) -(flet ($e239 (< ?e70 ?e7)) -(flet ($e240 (>= ?e13 ?e112)) -(flet ($e241 (p0 ?e24 ?e93)) -(flet ($e242 (<= ?e102 ?e87)) -(flet ($e243 (p0 ?e73 ?e25)) -(flet ($e244 (distinct ?e24 ?e116)) -(flet ($e245 (< ?e84 ?e78)) -(flet ($e246 (<= ?e104 ?e100)) -(flet ($e247 (= ?e18 ?e74)) -(flet ($e248 (< ?e16 ?e8)) -(flet ($e249 (< ?e93 ?e25)) -(flet ($e250 (>= ?e88 ?e81)) -(flet ($e251 (>= ?e98 ?e109)) -(flet ($e252 (>= ?e21 ?e13)) -(flet ($e253 (p0 v2 ?e74)) -(flet ($e254 (distinct ?e24 ?e27)) -(flet ($e255 (>= ?e120 ?e111)) -(flet ($e256 (>= ?e81 ?e14)) -(flet ($e257 (<= ?e87 ?e21)) -(flet ($e258 (p0 ?e74 ?e12)) -(flet ($e259 (distinct ?e5 ?e9)) -(flet ($e260 (>= ?e105 ?e79)) -(flet ($e261 (<= v2 ?e108)) -(flet ($e262 (= ?e96 ?e6)) -(flet ($e263 (= ?e5 ?e77)) -(flet ($e264 (>= v0 ?e23)) -(flet ($e265 (= ?e107 ?e72)) -(flet ($e266 (= ?e110 ?e95)) -(flet ($e267 (< ?e90 ?e117)) -(flet ($e268 (= v2 ?e23)) -(flet ($e269 (<= ?e77 ?e12)) -(flet ($e270 (<= ?e104 ?e111)) -(flet ($e271 (= ?e93 ?e14)) -(flet ($e272 (p0 ?e72 ?e79)) -(flet ($e273 (distinct ?e8 ?e20)) -(flet ($e274 (p0 ?e96 ?e112)) -(flet ($e275 (= ?e92 ?e24)) -(flet ($e276 (>= ?e16 ?e22)) -(flet ($e277 (= ?e19 ?e10)) -(flet ($e278 (<= ?e20 ?e86)) -(flet ($e279 (< ?e116 ?e118)) -(flet ($e280 (>= ?e74 ?e5)) -(flet ($e281 (<= ?e79 ?e105)) -(flet ($e282 (< ?e115 ?e70)) -(flet ($e283 (<= ?e13 ?e103)) -(flet ($e284 (p0 ?e27 ?e87)) -(flet ($e285 (p0 v0 ?e88)) -(flet ($e286 (<= ?e81 ?e104)) -(flet ($e287 (= ?e6 ?e99)) -(flet ($e288 (= ?e114 ?e87)) -(flet ($e289 (distinct ?e77 ?e71)) -(flet ($e290 (distinct ?e15 ?e15)) -(flet ($e291 (< ?e79 ?e72)) -(flet ($e292 (< ?e19 ?e8)) -(flet ($e293 (p0 ?e109 ?e5)) -(flet ($e294 (p0 v1 ?e19)) -(flet ($e295 (p0 ?e75 ?e104)) -(flet ($e296 (>= ?e100 ?e110)) -(flet ($e297 (>= ?e101 ?e23)) -(flet ($e298 (distinct ?e21 ?e107)) -(flet ($e299 (= ?e27 ?e101)) -(flet ($e300 (distinct ?e116 v1)) -(flet ($e301 (> ?e22 ?e5)) -(flet ($e302 (distinct ?e102 ?e80)) -(flet ($e303 (p0 ?e112 ?e84)) -(flet ($e304 (<= ?e111 ?e78)) -(flet ($e305 (= ?e75 ?e9)) -(flet ($e306 (= ?e80 ?e20)) -(flet ($e307 (< ?e80 ?e80)) -(flet ($e308 (distinct ?e13 ?e9)) -(flet ($e309 (p0 ?e6 ?e14)) -(flet ($e310 (> ?e70 ?e91)) -(flet ($e311 (> ?e16 ?e8)) -(flet ($e312 (<= ?e13 ?e95)) -(flet ($e313 (> ?e92 ?e95)) -(flet ($e314 (< ?e96 ?e87)) -(flet ($e315 (= ?e91 ?e92)) -(flet ($e316 (>= ?e120 ?e117)) -(flet ($e317 (p0 ?e13 ?e93)) -(flet ($e318 (distinct ?e120 ?e24)) -(flet ($e319 (>= ?e15 ?e86)) -(flet ($e320 (> ?e94 ?e84)) -(flet ($e321 (> ?e20 ?e99)) -(flet ($e322 (< ?e23 ?e71)) -(flet ($e323 (= ?e119 ?e73)) -(flet ($e324 (<= ?e82 ?e94)) -(flet ($e325 (<= ?e108 ?e107)) -(flet ($e326 (p0 ?e13 ?e80)) -(flet ($e327 (<= ?e87 ?e102)) -(flet ($e328 (<= ?e74 ?e89)) -(flet ($e329 (= ?e73 ?e11)) -(flet ($e330 (distinct ?e15 ?e106)) -(flet ($e331 (<= ?e115 ?e110)) -(flet ($e332 (p0 v0 ?e69)) -(flet ($e333 (>= v1 ?e9)) -(flet ($e334 (> v1 v2)) -(flet ($e335 (< ?e80 ?e95)) -(flet ($e336 (>= ?e114 ?e69)) -(flet ($e337 (distinct ?e80 ?e118)) -(flet ($e338 (p0 ?e16 ?e91)) -(flet ($e339 (p0 ?e100 ?e85)) -(flet ($e340 (= ?e13 ?e73)) -(flet ($e341 (= ?e92 ?e12)) -(flet ($e342 (p0 ?e100 ?e72)) -(flet ($e343 (= ?e26 ?e119)) -(flet ($e344 (< ?e20 ?e20)) -(flet ($e345 (<= ?e100 ?e94)) -(flet ($e346 (> ?e114 ?e116)) -(flet ($e347 (p0 ?e102 ?e19)) -(flet ($e348 (= ?e113 ?e13)) -(flet ($e349 (distinct ?e108 ?e5)) -(flet ($e350 (< ?e14 ?e118)) -(flet ($e351 (< ?e72 ?e110)) -(flet ($e352 (> ?e83 ?e114)) -(flet ($e353 (distinct ?e106 ?e24)) -(flet ($e354 (<= ?e24 ?e83)) -(flet ($e355 (p0 ?e116 ?e101)) -(flet ($e356 (< ?e110 ?e96)) -(flet ($e357 (= ?e12 v0)) -(flet ($e358 (p0 ?e108 ?e113)) -(flet ($e359 (>= ?e27 ?e81)) -(flet ($e360 (<= ?e109 ?e75)) -(flet ($e361 (= ?e102 ?e26)) -(flet ($e362 (distinct ?e108 ?e104)) -(flet ($e363 (<= ?e108 ?e26)) -(flet ($e364 (<= ?e114 ?e69)) -(flet ($e365 (>= ?e113 ?e82)) -(flet ($e366 (= ?e115 v1)) -(flet ($e367 (= ?e25 ?e27)) -(flet ($e368 (p0 ?e27 ?e91)) -(flet ($e369 (<= ?e13 ?e116)) -(flet ($e370 (<= ?e87 ?e114)) -(flet ($e371 (< ?e25 ?e108)) -(flet ($e372 (= ?e108 ?e9)) -(flet ($e373 (p0 ?e89 ?e117)) -(flet ($e374 (<= ?e13 ?e19)) -(flet ($e375 (p0 ?e12 ?e26)) -(flet ($e376 (< ?e20 ?e91)) -(flet ($e377 (distinct ?e107 ?e76)) -(flet ($e378 (if_then_else $e180 $e123 $e342)) -(flet ($e379 (if_then_else $e151 $e330 $e232)) -(flet ($e380 (if_then_else $e136 $e175 $e130)) -(flet ($e381 (if_then_else $e362 $e250 $e56)) -(flet ($e382 (not $e337)) -(flet ($e383 (xor $e194 $e150)) -(flet ($e384 (iff $e44 $e65)) -(flet ($e385 (xor $e300 $e160)) -(flet ($e386 (xor $e158 $e241)) -(flet ($e387 (not $e286)) -(flet ($e388 (and $e168 $e55)) -(flet ($e389 (or $e143 $e153)) -(flet ($e390 (not $e289)) -(flet ($e391 (or $e191 $e235)) -(flet ($e392 (and $e42 $e184)) -(flet ($e393 (not $e170)) -(flet ($e394 (iff $e35 $e356)) -(flet ($e395 (xor $e128 $e207)) -(flet ($e396 (implies $e394 $e208)) -(flet ($e397 (not $e354)) -(flet ($e398 (not $e201)) -(flet ($e399 (if_then_else $e176 $e169 $e331)) -(flet ($e400 (and $e217 $e172)) -(flet ($e401 (and $e324 $e178)) -(flet ($e402 (iff $e387 $e279)) -(flet ($e403 (or $e204 $e374)) -(flet ($e404 (iff $e323 $e334)) -(flet ($e405 (xor $e302 $e247)) -(flet ($e406 (iff $e288 $e125)) -(flet ($e407 (or $e375 $e227)) -(flet ($e408 (and $e127 $e378)) -(flet ($e409 (iff $e58 $e284)) -(flet ($e410 (implies $e181 $e52)) -(flet ($e411 (implies $e166 $e385)) -(flet ($e412 (and $e41 $e306)) -(flet ($e413 (xor $e268 $e361)) -(flet ($e414 (and $e47 $e32)) -(flet ($e415 (iff $e228 $e339)) -(flet ($e416 (implies $e292 $e199)) -(flet ($e417 (implies $e252 $e39)) -(flet ($e418 (or $e37 $e351)) -(flet ($e419 (and $e209 $e49)) -(flet ($e420 (implies $e263 $e197)) -(flet ($e421 (if_then_else $e349 $e312 $e287)) -(flet ($e422 (implies $e353 $e249)) -(flet ($e423 (not $e388)) -(flet ($e424 (and $e296 $e310)) -(flet ($e425 (xor $e309 $e59)) -(flet ($e426 (and $e240 $e242)) -(flet ($e427 (if_then_else $e45 $e163 $e411)) -(flet ($e428 (not $e364)) -(flet ($e429 (if_then_else $e144 $e267 $e293)) -(flet ($e430 (if_then_else $e173 $e238 $e126)) -(flet ($e431 (implies $e338 $e48)) -(flet ($e432 (iff $e156 $e383)) -(flet ($e433 (or $e68 $e391)) -(flet ($e434 (xor $e262 $e304)) -(flet ($e435 (not $e318)) -(flet ($e436 (iff $e29 $e155)) -(flet ($e437 (not $e121)) -(flet ($e438 (implies $e389 $e36)) -(flet ($e439 (iff $e234 $e174)) -(flet ($e440 (iff $e253 $e314)) -(flet ($e441 (if_then_else $e137 $e278 $e355)) -(flet ($e442 (xor $e131 $e64)) -(flet ($e443 (or $e377 $e124)) -(flet ($e444 (implies $e346 $e122)) -(flet ($e445 (iff $e212 $e372)) -(flet ($e446 (implies $e195 $e277)) -(flet ($e447 (not $e430)) -(flet ($e448 (not $e192)) -(flet ($e449 (implies $e196 $e177)) -(flet ($e450 (or $e190 $e257)) -(flet ($e451 (iff $e215 $e412)) -(flet ($e452 (implies $e274 $e418)) -(flet ($e453 (if_then_else $e336 $e322 $e149)) -(flet ($e454 (if_then_else $e447 $e189 $e269)) -(flet ($e455 (not $e218)) -(flet ($e456 (xor $e152 $e224)) -(flet ($e457 (not $e358)) -(flet ($e458 (not $e60)) -(flet ($e459 (not $e424)) -(flet ($e460 (not $e398)) -(flet ($e461 (if_then_else $e380 $e291 $e453)) -(flet ($e462 (iff $e305 $e271)) -(flet ($e463 (if_then_else $e408 $e417 $e148)) -(flet ($e464 (not $e270)) -(flet ($e465 (and $e261 $e51)) -(flet ($e466 (or $e450 $e299)) -(flet ($e467 (iff $e301 $e154)) -(flet ($e468 (iff $e200 $e460)) -(flet ($e469 (and $e343 $e129)) -(flet ($e470 (iff $e313 $e400)) -(flet ($e471 (or $e433 $e347)) -(flet ($e472 (not $e451)) -(flet ($e473 (iff $e266 $e317)) -(flet ($e474 (and $e273 $e390)) -(flet ($e475 (and $e406 $e440)) -(flet ($e476 (implies $e223 $e233)) -(flet ($e477 (if_then_else $e298 $e185 $e344)) -(flet ($e478 (xor $e462 $e426)) -(flet ($e479 (and $e368 $e28)) -(flet ($e480 (implies $e319 $e466)) -(flet ($e481 (not $e348)) -(flet ($e482 (not $e134)) -(flet ($e483 (xor $e145 $e471)) -(flet ($e484 (xor $e439 $e171)) -(flet ($e485 (if_then_else $e369 $e198 $e295)) -(flet ($e486 (xor $e329 $e405)) -(flet ($e487 (iff $e290 $e221)) -(flet ($e488 (if_then_else $e373 $e415 $e219)) -(flet ($e489 (iff $e50 $e244)) -(flet ($e490 (and $e363 $e403)) -(flet ($e491 (or $e402 $e431)) -(flet ($e492 (not $e229)) -(flet ($e493 (implies $e470 $e280)) -(flet ($e494 (or $e489 $e220)) -(flet ($e495 (and $e188 $e67)) -(flet ($e496 (or $e53 $e165)) -(flet ($e497 (and $e427 $e206)) -(flet ($e498 (iff $e307 $e333)) -(flet ($e499 (if_then_else $e186 $e487 $e281)) -(flet ($e500 (iff $e360 $e442)) -(flet ($e501 (iff $e490 $e357)) -(flet ($e502 (iff $e392 $e211)) -(flet ($e503 (xor $e210 $e410)) -(flet ($e504 (iff $e239 $e486)) -(flet ($e505 (implies $e248 $e54)) -(flet ($e506 (implies $e465 $e492)) -(flet ($e507 (and $e494 $e255)) -(flet ($e508 (or $e285 $e352)) -(flet ($e509 (if_then_else $e264 $e399 $e316)) -(flet ($e510 (if_then_else $e34 $e508 $e448)) -(flet ($e511 (not $e203)) -(flet ($e512 (not $e246)) -(flet ($e513 (and $e366 $e371)) -(flet ($e514 (xor $e367 $e311)) -(flet ($e515 (iff $e141 $e226)) -(flet ($e516 (iff $e455 $e484)) -(flet ($e517 (iff $e164 $e62)) -(flet ($e518 (iff $e140 $e294)) -(flet ($e519 (and $e345 $e222)) -(flet ($e520 (xor $e135 $e519)) -(flet ($e521 (implies $e216 $e315)) -(flet ($e522 (or $e260 $e446)) -(flet ($e523 (xor $e520 $e522)) -(flet ($e524 (iff $e407 $e46)) -(flet ($e525 (xor $e275 $e256)) -(flet ($e526 (and $e420 $e423)) -(flet ($e527 (not $e61)) -(flet ($e528 (implies $e297 $e488)) -(flet ($e529 (or $e231 $e332)) -(flet ($e530 (and $e482 $e66)) -(flet ($e531 (and $e518 $e245)) -(flet ($e532 (not $e183)) -(flet ($e533 (and $e382 $e236)) -(flet ($e534 (iff $e456 $e422)) -(flet ($e535 (if_then_else $e413 $e524 $e379)) -(flet ($e536 (and $e436 $e401)) -(flet ($e537 (xor $e475 $e475)) -(flet ($e538 (implies $e437 $e498)) -(flet ($e539 (implies $e485 $e477)) -(flet ($e540 (implies $e504 $e474)) -(flet ($e541 (xor $e272 $e445)) -(flet ($e542 (implies $e393 $e438)) -(flet ($e543 (xor $e139 $e205)) -(flet ($e544 (implies $e414 $e386)) -(flet ($e545 (if_then_else $e214 $e321 $e544)) -(flet ($e546 (xor $e449 $e265)) -(flet ($e547 (and $e533 $e187)) -(flet ($e548 (xor $e530 $e506)) -(flet ($e549 (or $e258 $e283)) -(flet ($e550 (iff $e326 $e500)) -(flet ($e551 (if_then_else $e535 $e359 $e537)) -(flet ($e552 (iff $e479 $e469)) -(flet ($e553 (xor $e531 $e521)) -(flet ($e554 (xor $e435 $e43)) -(flet ($e555 (not $e162)) -(flet ($e556 (and $e525 $e454)) -(flet ($e557 (xor $e501 $e514)) -(flet ($e558 (implies $e179 $e138)) -(flet ($e559 (xor $e404 $e365)) -(flet ($e560 (not $e540)) -(flet ($e561 (xor $e513 $e546)) -(flet ($e562 (implies $e503 $e308)) -(flet ($e563 (if_then_else $e541 $e561 $e434)) -(flet ($e564 (not $e335)) -(flet ($e565 (not $e341)) -(flet ($e566 (if_then_else $e564 $e551 $e511)) -(flet ($e567 (or $e523 $e496)) -(flet ($e568 (and $e534 $e159)) -(flet ($e569 (if_then_else $e555 $e562 $e497)) -(flet ($e570 (xor $e457 $e225)) -(flet ($e571 (or $e161 $e251)) -(flet ($e572 (implies $e556 $e559)) -(flet ($e573 (iff $e483 $e370)) -(flet ($e574 (if_then_else $e237 $e432 $e213)) -(flet ($e575 (and $e147 $e528)) -(flet ($e576 (xor $e376 $e552)) -(flet ($e577 (and $e463 $e542)) -(flet ($e578 (not $e548)) -(flet ($e579 (implies $e468 $e560)) -(flet ($e580 (or $e557 $e495)) -(flet ($e581 (if_then_else $e327 $e478 $e472)) -(flet ($e582 (implies $e254 $e572)) -(flet ($e583 (and $e491 $e543)) -(flet ($e584 (implies $e527 $e243)) -(flet ($e585 (if_then_else $e428 $e142 $e566)) -(flet ($e586 (xor $e429 $e133)) -(flet ($e587 (not $e202)) -(flet ($e588 (iff $e481 $e550)) -(flet ($e589 (iff $e33 $e441)) -(flet ($e590 (or $e547 $e532)) -(flet ($e591 (and $e538 $e57)) -(flet ($e592 (not $e230)) -(flet ($e593 (or $e576 $e592)) -(flet ($e594 (iff $e505 $e578)) -(flet ($e595 (and $e350 $e580)) -(flet ($e596 (or $e443 $e574)) -(flet ($e597 (or $e579 $e575)) -(flet ($e598 (or $e132 $e38)) -(flet ($e599 (implies $e303 $e146)) -(flet ($e600 (if_then_else $e598 $e499 $e419)) -(flet ($e601 (and $e558 $e473)) -(flet ($e602 (or $e590 $e529)) -(flet ($e603 (if_then_else $e591 $e182 $e40)) -(flet ($e604 (iff $e596 $e571)) -(flet ($e605 (iff $e328 $e588)) -(flet ($e606 (and $e397 $e594)) -(flet ($e607 (or $e593 $e502)) -(flet ($e608 (or $e516 $e539)) -(flet ($e609 (iff $e573 $e193)) -(flet ($e610 (not $e549)) -(flet ($e611 (not $e563)) -(flet ($e612 (xor $e30 $e606)) -(flet ($e613 (if_then_else $e467 $e609 $e581)) -(flet ($e614 (not $e526)) -(flet ($e615 (if_then_else $e517 $e602 $e610)) -(flet ($e616 (implies $e464 $e396)) -(flet ($e617 (not $e425)) -(flet ($e618 (or $e452 $e611)) -(flet ($e619 (xor $e416 $e63)) -(flet ($e620 (iff $e545 $e565)) -(flet ($e621 (xor $e603 $e458)) -(flet ($e622 (if_then_else $e536 $e476 $e567)) -(flet ($e623 (or $e515 $e157)) -(flet ($e624 (iff $e510 $e493)) -(flet ($e625 (or $e600 $e599)) -(flet ($e626 (iff $e553 $e619)) -(flet ($e627 (or $e586 $e625)) -(flet ($e628 (not $e621)) -(flet ($e629 (not $e509)) -(flet ($e630 (xor $e617 $e582)) -(flet ($e631 (implies $e480 $e630)) -(flet ($e632 (implies $e421 $e340)) -(flet ($e633 (iff $e577 $e612)) -(flet ($e634 (iff $e512 $e627)) -(flet ($e635 (if_then_else $e632 $e444 $e583)) -(flet ($e636 (not $e569)) -(flet ($e637 (implies $e629 $e276)) -(flet ($e638 (and $e633 $e620)) -(flet ($e639 (and $e461 $e381)) -(flet ($e640 (iff $e597 $e395)) -(flet ($e641 (implies $e637 $e639)) -(flet ($e642 (and $e640 $e320)) -(flet ($e643 (or $e607 $e259)) -(flet ($e644 (if_then_else $e384 $e584 $e325)) -(flet ($e645 (implies $e626 $e608)) -(flet ($e646 (xor $e585 $e631)) -(flet ($e647 (or $e616 $e167)) -(flet ($e648 (or $e568 $e644)) -(flet ($e649 (or $e589 $e614)) -(flet ($e650 (and $e641 $e642)) -(flet ($e651 (xor $e554 $e650)) -(flet ($e652 (implies $e635 $e595)) -(flet ($e653 (or $e618 $e636)) -(flet ($e654 (and $e645 $e282)) -(flet ($e655 (not $e648)) -(flet ($e656 (or $e649 $e652)) -(flet ($e657 (iff $e31 $e409)) -(flet ($e658 (iff $e634 $e651)) -(flet ($e659 (xor $e601 $e605)) -(flet ($e660 (not $e628)) -(flet ($e661 (xor $e587 $e622)) -(flet ($e662 (not $e459)) -(flet ($e663 (or $e656 $e638)) -(flet ($e664 (not $e646)) -(flet ($e665 (or $e623 $e653)) -(flet ($e666 (implies $e663 $e663)) -(flet ($e667 (implies $e570 $e507)) -(flet ($e668 (xor $e647 $e658)) -(flet ($e669 (not $e661)) -(flet ($e670 (iff $e660 $e657)) -(flet ($e671 (not $e655)) -(flet ($e672 (if_then_else $e615 $e615 $e624)) -(flet ($e673 (iff $e665 $e643)) -(flet ($e674 (xor $e662 $e669)) -(flet ($e675 (not $e671)) -(flet ($e676 (and $e674 $e675)) -(flet ($e677 (implies $e670 $e676)) -(flet ($e678 (iff $e668 $e604)) -(flet ($e679 (not $e659)) -(flet ($e680 (or $e672 $e666)) -(flet ($e681 (xor $e679 $e678)) -(flet ($e682 (not $e667)) -(flet ($e683 (and $e677 $e681)) -(flet ($e684 (xor $e680 $e680)) -(flet ($e685 (not $e683)) -(flet ($e686 (if_then_else $e664 $e684 $e685)) -(flet ($e687 (iff $e654 $e686)) -(flet ($e688 (if_then_else $e687 $e613 $e613)) -(flet ($e689 (and $e682 $e688)) -(flet ($e690 (implies $e673 $e689)) -$e690 -))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - diff --git a/test/regress/regress0/uflia/error1.smtv1.smt2 b/test/regress/regress0/uflia/error1.smtv1.smt2 new file mode 100644 index 000000000..a652ad707 --- /dev/null +++ b/test/regress/regress0/uflia/error1.smtv1.smt2 @@ -0,0 +1,10 @@ +(set-option :incremental false) +(set-info :status sat) +(set-logic QF_UFLIA) +(declare-fun f0 (Int Int Int) Int) +(declare-fun f1 (Int) Int) +(declare-fun p0 (Int Int) Bool) +(declare-fun v0 () Int) +(declare-fun v1 () Int) +(declare-fun v2 () Int) +(check-sat-assuming ( (let ((_let_0 (ite (p0 (+ v2 v2) v1) 1 0))) (let ((_let_1 (ite (p0 (f1 v1) v1) 1 0))) (let ((_let_2 (ite (p0 v2 _let_1) 1 0))) (let ((_let_3 (* (- 2) (+ v2 v2)))) (let ((_let_4 (+ v1 (f1 v1)))) (let ((_let_5 (* 2 _let_3))) (let ((_let_6 (f0 v2 (f1 v1) v0))) (let ((_let_7 (+ (ite (p0 v1 (+ v2 v2)) 1 0) _let_3))) (let ((_let_8 (- _let_4 _let_3))) (let ((_let_9 (* _let_8 (- 2)))) (let ((_let_10 (- (+ v2 v2)))) (let ((_let_11 (f1 (+ v2 v2)))) (let ((_let_12 (> _let_0 _let_3))) (let ((_let_13 (= v2 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (let ((_let_14 (< _let_3 (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0)))) (let ((_let_15 (distinct _let_1 _let_9))) (let ((_let_16 (>= v0 (+ _let_4 _let_7)))) (let ((_let_17 (distinct _let_11 (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))))) (let ((_let_18 (distinct (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) (+ _let_4 _let_7)))) (let ((_let_19 (ite (> _let_7 (f1 v1)) (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_3))) (let ((_let_20 (ite _let_14 (+ (+ v2 v2) _let_1) _let_8))) (let ((_let_21 (ite (< _let_1 _let_2) (+ (+ v2 v2) _let_1) _let_10))) (let ((_let_22 (ite (p0 v1 _let_9) v2 _let_10))) (let ((_let_23 (ite (<= v2 v2) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) _let_6))) (let ((_let_24 (ite (= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) (* _let_10 (- 1))) (+ _let_4 _let_7) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))))) (let ((_let_25 (ite _let_18 v0 _let_2))) (let ((_let_26 (ite (distinct (f1 v1) _let_10) (+ v2 v2) v0))) (let ((_let_27 (ite (> _let_3 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_20 _let_4))) (let ((_let_28 (ite (> _let_4 _let_6) _let_8 _let_9))) (let ((_let_29 (ite _let_16 (ite _let_12 _let_26 v2) v2))) (let ((_let_30 (ite _let_14 _let_0 _let_6))) (let ((_let_31 (ite (> _let_6 _let_8) (* _let_10 (- 1)) (* _let_10 (- 1))))) (let ((_let_32 (ite (>= _let_6 _let_0) (ite (p0 v1 (+ v2 v2)) 1 0) _let_3))) (let ((_let_33 (ite (<= _let_4 _let_3) _let_11 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (let ((_let_34 (ite (< _let_0 (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) v1))) (let ((_let_35 (ite (distinct _let_0 (+ (+ v2 v2) _let_1)) (ite _let_18 _let_7 v0) _let_6))) (let ((_let_36 (ite _let_16 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1)) (* _let_10 (- 1))))) (let ((_let_37 (ite _let_18 _let_10 _let_21))) (let ((_let_38 (ite (distinct _let_2 _let_9) (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2)) _let_5))) (let ((_let_39 (ite (= _let_3 _let_1) _let_32 _let_0))) (let ((_let_40 (ite _let_12 (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21) (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1))))) (let ((_let_41 (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (p0 v1 (+ v2 v2)) 1 0)) _let_0 _let_27))) (let ((_let_42 (ite (< _let_4 (+ v2 v2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (let ((_let_43 (ite (<= v2 v2) (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) _let_27))) (let ((_let_44 (ite (distinct (+ _let_4 _let_7) (+ _let_4 _let_7)) _let_2 (ite (p0 v1 (+ v2 v2)) 1 0)))) (let ((_let_45 (ite _let_15 _let_42 _let_24))) (let ((_let_46 (ite (>= _let_1 _let_2) _let_40 (ite _let_18 _let_7 v0)))) (let ((_let_47 (ite (> _let_4 _let_6) (+ _let_4 _let_7) (ite (> (+ _let_4 _let_7) (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25) _let_21)))) (let ((_let_48 (ite (< _let_0 (+ v2 v2)) (ite (>= (+ v2 v2) (* _let_10 (- 1))) _let_1 _let_33) _let_9))) (let ((_let_49 (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_48 (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1))))) (let ((_let_50 (ite _let_17 _let_0 _let_10))) (let ((_let_51 (ite (< _let_2 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_0 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))))) (let ((_let_52 (ite _let_13 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1)) (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (let ((_let_53 (ite (= _let_7 (f1 v1)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) _let_11))) (let ((_let_54 (ite (>= v1 (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) _let_24 _let_10))) (let ((_let_55 (and (= (= (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) _let_31) (>= (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21) _let_7)) (= (p0 v2 (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9)) (< (ite (< _let_1 _let_2) _let_26 _let_8) _let_31))))) (let ((_let_56 (ite (= (> (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f1 v1)) (= (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2))) (= (= (xor (= (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_5 _let_5) (ite (= _let_3 _let_1) _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) (or (or (>= v1 (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) (or (> _let_5 (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21)) (distinct (ite (< _let_1 _let_2) _let_26 _let_8) _let_6))) (p0 _let_40 _let_8))) (<= _let_31 (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)))) (distinct _let_3 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) (ite (<= _let_31 _let_40) (xor (= (= (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1)) (+ (+ v2 v2) _let_1)) (= (ite (>= (+ v2 v2) (* _let_10 (- 1))) _let_1 _let_33) _let_5)) (and (>= _let_4 _let_47) (<= _let_40 _let_31))) (not (= (p0 (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2)) _let_47) (and _let_12 (= (ite _let_18 _let_7 v0) _let_9)))))))) (let ((_let_57 (or (ite (ite (= (<= (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1)) _let_2) _let_18) (or (or (and (and (not (distinct (ite _let_18 _let_7 v0) _let_52)) (distinct (ite (< _let_1 _let_2) _let_26 _let_8) _let_0)) (<= (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21) (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_5 _let_5))) (not (<= _let_4 (+ (+ v2 v2) _let_1)))) (or (< (ite _let_12 _let_26 v2) _let_9) (p0 v0 _let_19))) (not (or (p0 (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) _let_3) (<= _let_4 _let_41)))) (ite (= (<= (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1)) _let_2) _let_18) (or (or (and (and (not (distinct (ite _let_18 _let_7 v0) _let_52)) (distinct (ite (< _let_1 _let_2) _let_26 _let_8) _let_0)) (<= (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21) (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_5 _let_5))) (not (<= _let_4 (+ (+ v2 v2) _let_1)))) (or (< (ite _let_12 _let_26 v2) _let_9) (p0 v0 _let_19))) (not (or (p0 (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) _let_3) (<= _let_4 _let_41)))) (= (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (or (p0 v0 (ite (= _let_3 _let_1) _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) (> (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25) (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)))) (not (< _let_39 (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2))))) (=> (= (> _let_34 _let_36) (and (= _let_54 _let_39) (>= _let_3 (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25))))) (>= (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) (f1 v1))))) (=> (or (or (or (= (distinct _let_2 _let_9) (ite (distinct _let_20 _let_35) (<= _let_9 _let_30) (p0 _let_50 _let_39))) (not (and (=> (= (f1 v1) _let_25) (p0 _let_50 _let_4)) (not (and (< _let_19 _let_26) (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))))))) (=> (ite (=> (ite (distinct _let_45 (f1 v1)) (<= _let_4 _let_36) (= (+ v2 v2) (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)))) (= _let_4 _let_23)) (=> (> (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) _let_50) (distinct (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) v0)) (and (or (= (not (<= _let_27 _let_42)) (< _let_50 _let_52)) (=> (p0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_33) (< _let_4 (+ v2 v2)))) (xor (= _let_44 (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1))) (distinct _let_10 _let_6)))) (and (< _let_5 _let_52) (or (xor (= (and (<= _let_45 _let_11) (or (> (* _let_10 (- 1)) _let_10) (<= _let_4 _let_8))) (= _let_3 v0)) (xor (= _let_10 (* _let_10 (- 1))) (> (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_1))) (and (distinct (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1)) (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2))) (distinct (+ _let_4 _let_7) (+ _let_4 _let_7))))))) (and (= (and (ite (and (<= (ite _let_12 _let_26 v2) _let_44) (ite (>= _let_46 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2)) (= _let_50 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (p0 _let_38 _let_22))) (=> (>= (+ _let_4 _let_7) _let_4) (= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) (* _let_10 (- 1)))) (<= _let_31 _let_30)) (=> (not (= _let_51 (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (=> (or (< _let_38 _let_35) (p0 (ite _let_12 _let_26 v2) (ite (< _let_1 _let_2) _let_26 _let_8))) (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (p0 v1 (+ v2 v2)) 1 0))))) (xor (distinct _let_0 (+ (+ v2 v2) _let_1)) (and (not (<= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25))) (= (=> (< (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_1) (> _let_4 _let_6)) (not (xor (and (not (<= _let_38 (+ _let_4 _let_7))) (= (+ _let_4 _let_7) (+ v2 v2))) (=> (and (<= v2 _let_45) (>= _let_6 _let_0)) (not (>= (ite (p0 v1 (+ v2 v2)) 1 0) _let_1))))))))) (= (ite (>= _let_22 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2)) (> _let_9 (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7))) (=> (and _let_14 (>= (+ v2 v2) (* _let_10 (- 1)))) (xor (< (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) _let_32) (p0 (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (>= (+ v2 v2) (* _let_10 (- 1))) _let_1 _let_33))))) (not (= _let_34 _let_3))))) (or (or (or (= (distinct _let_2 _let_9) (ite (distinct _let_20 _let_35) (<= _let_9 _let_30) (p0 _let_50 _let_39))) (not (and (=> (= (f1 v1) _let_25) (p0 _let_50 _let_4)) (not (and (< _let_19 _let_26) (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))))))) (=> (ite (=> (ite (distinct _let_45 (f1 v1)) (<= _let_4 _let_36) (= (+ v2 v2) (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)))) (= _let_4 _let_23)) (=> (> (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) _let_50) (distinct (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) v0)) (and (or (= (not (<= _let_27 _let_42)) (< _let_50 _let_52)) (=> (p0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_33) (< _let_4 (+ v2 v2)))) (xor (= _let_44 (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1))) (distinct _let_10 _let_6)))) (and (< _let_5 _let_52) (or (xor (= (and (<= _let_45 _let_11) (or (> (* _let_10 (- 1)) _let_10) (<= _let_4 _let_8))) (= _let_3 v0)) (xor (= _let_10 (* _let_10 (- 1))) (> (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_1))) (and (distinct (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1)) (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2))) (distinct (+ _let_4 _let_7) (+ _let_4 _let_7))))))) (and (= (and (ite (and (<= (ite _let_12 _let_26 v2) _let_44) (ite (>= _let_46 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2)) (= _let_50 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (p0 _let_38 _let_22))) (=> (>= (+ _let_4 _let_7) _let_4) (= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) (* _let_10 (- 1)))) (<= _let_31 _let_30)) (=> (not (= _let_51 (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (=> (or (< _let_38 _let_35) (p0 (ite _let_12 _let_26 v2) (ite (< _let_1 _let_2) _let_26 _let_8))) (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (p0 v1 (+ v2 v2)) 1 0))))) (xor (distinct _let_0 (+ (+ v2 v2) _let_1)) (and (not (<= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25))) (= (=> (< (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_1) (> _let_4 _let_6)) (not (xor (and (not (<= _let_38 (+ _let_4 _let_7))) (= (+ _let_4 _let_7) (+ v2 v2))) (=> (and (<= v2 _let_45) (>= _let_6 _let_0)) (not (>= (ite (p0 v1 (+ v2 v2)) 1 0) _let_1))))))))) (= (ite (>= _let_22 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2)) (> _let_9 (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7))) (=> (and _let_14 (>= (+ v2 v2) (* _let_10 (- 1)))) (xor (< (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) _let_32) (p0 (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (>= (+ v2 v2) (* _let_10 (- 1))) _let_1 _let_33))))) (not (= _let_34 _let_3))))))))) (=> (= (or (or (= (< (+ _let_4 _let_7) (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25))) (<= _let_33 (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9))) (= _let_8 _let_37)) (or (or (=> (p0 (ite (< _let_1 _let_2) _let_26 _let_8) _let_47) (or (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (< _let_22 _let_46))) (not (ite (xor (p0 _let_22 _let_26) (= (p0 _let_4 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (= _let_45 (+ (+ v2 v2) _let_1)))) (xor (and (= _let_49 v1) (< _let_10 _let_45)) (xor (=> (>= _let_41 _let_3) (> (ite (p0 v1 (+ v2 v2)) 1 0) _let_7)) (= _let_44 _let_22))) (xor (= (ite (< _let_1 _let_2) _let_26 _let_8) (+ v2 v2)) (<= (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2) (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21)))))) (not (ite (not (< (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) (+ v2 v2))) (=> (xor (distinct _let_4 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))) (=> (< v0 _let_31) _let_15)) (distinct _let_4 (+ (+ v2 v2) _let_1))) (and (ite (= _let_3 _let_1) (> (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) _let_50) (=> (> (* _let_10 (- 1)) (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2))) (xor (distinct _let_50 v1) (<= v2 _let_54)))) (distinct v1 _let_29)))))) (or (or (or (xor (< _let_9 _let_33) (= (and (p0 (* _let_10 (- 1)) _let_33) (< _let_0 (+ v2 v2))) (and (= _let_11 _let_53) (= _let_36 _let_26)))) (not (> _let_46 _let_22))) (= (and (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) (>= _let_0 _let_9)) (= _let_33 _let_19))) (distinct (f1 v1) (+ (+ v2 v2) _let_1)))) (and (not (=> (xor (not (p0 _let_45 _let_48)) (>= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9))) (and (or (= (> _let_10 _let_7) (distinct (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) _let_50)) (< _let_51 _let_48)) (>= _let_54 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2))))) (ite (= (and (=> (= (xor (and (= (p0 _let_46 v2) (p0 v1 _let_8)) (< (ite _let_12 _let_26 v2) (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21))) (=> (>= (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21) _let_37) (= _let_33 _let_34))) (xor (=> (< _let_8 _let_1) (p0 _let_44 _let_54)) (p0 v1 _let_9))) (or (= (not (<= _let_22 _let_21)) (xor (= (p0 _let_5 _let_32) (<= _let_22 _let_53)) (>= _let_22 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (=> (ite (<= _let_4 _let_50) (>= _let_29 _let_4) (p0 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1)) _let_42)) (ite (distinct (+ _let_4 _let_7) _let_44) (<= _let_25 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (< _let_9 _let_9))))) (< _let_49 _let_20)) (ite (not (xor (ite (not (<= (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) _let_19)) (p0 _let_9 v2) (ite (not (< (ite _let_18 _let_7 v0) _let_36)) (ite (ite (xor (= v2 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (= _let_40 _let_11)) (= (or (p0 _let_3 _let_11) (p0 v2 _let_20)) (<= _let_4 _let_3)) (ite (distinct _let_36 _let_21) (distinct _let_6 (ite (> (+ _let_4 _let_7) (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25) _let_21)) (p0 _let_26 _let_11))) (>= (* _let_10 (- 1)) _let_27) (xor _let_55 _let_55)) (not (>= _let_22 _let_2)))) (=> (=> (>= _let_6 _let_30) (or (or (> _let_27 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2)) (<= _let_31 (+ _let_4 _let_7))) (= (* _let_10 (- 1)) _let_39))) (xor (not (xor (p0 (+ v2 v2) _let_5) (> _let_7 (f1 v1)))) (=> (distinct (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* _let_10 (- 1))) (=> (and (xor (= _let_34 (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0)) (>= _let_27 _let_5)) (ite (not (ite (distinct _let_53 (* _let_10 (- 1))) (= _let_46 _let_21) (> (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))))) (p0 _let_52 (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2))) (<= _let_25 _let_3))) (xor (= (= _let_53 _let_23) (> v1 v2)) (>= _let_48 _let_28)))))))) (xor _let_57 _let_57) (not (and (=> (= (not (not (xor (ite (and (=> (not (< _let_32 (+ (+ v2 v2) _let_1))) (= (< (ite _let_18 _let_7 v0) (ite _let_18 _let_7 v0)) (>= v1 (+ (+ v2 v2) _let_1)))) (= v1 (ite (p0 v1 (+ v2 v2)) 1 0))) (< _let_22 _let_20) (> (+ _let_4 _let_7) (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) (not (< _let_2 (ite (p0 v1 (+ v2 v2)) 1 0)))))) (= (<= v2 v2) (= _let_17 (p0 (* _let_10 (- 1)) _let_31)))) (and (xor (not (not (and (>= _let_38 _let_46) (> _let_20 _let_33)))) (not (xor (not (>= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_41)) (ite (and (= (> _let_3 (ite (p0 v1 (+ v2 v2)) 1 0)) (p0 _let_5 _let_52)) (and (<= _let_28 _let_35) (> _let_49 _let_6))) (=> (< _let_25 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2)) (= _let_48 _let_27)) (or (xor (xor (= _let_40 _let_7) (and (<= _let_38 _let_35) (> _let_2 _let_42))) (or (>= _let_43 _let_26) (=> (>= _let_38 _let_31) (= _let_8 (ite (p0 v1 (+ v2 v2)) 1 0))))) (or (= _let_7 (f1 v1)) (distinct (+ (+ v2 v2) _let_1) (ite (p0 v1 (+ v2 v2)) 1 0)))))))) (not (not (not (or (and (= (xor (distinct _let_8 _let_39) (<= (+ _let_4 _let_7) _let_0)) (=> (distinct (ite (> (+ _let_4 _let_7) (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25) _let_21) (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0)) (< (ite (>= (+ v2 v2) (* _let_10 (- 1))) _let_1 _let_33) _let_10))) (>= _let_5 _let_6)) (ite (= (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) (<= _let_11 _let_3)) (=> (not (>= _let_1 _let_2)) (p0 _let_23 _let_10)) (<= _let_45 _let_44)))))))) (xor (not (xor (and (=> (= _let_4 _let_22) (= (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) _let_47)) (= (= _let_46 _let_36) (p0 _let_4 (ite (>= (+ v2 v2) (* _let_10 (- 1))) _let_1 _let_33)))) (= (<= (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1))) (= (not (= _let_48 _let_4)) (= (p0 _let_4 (ite _let_18 _let_7 v0)) (= (<= (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_5 _let_5) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))) (xor (<= (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25) _let_42) (< _let_1 _let_2)))))))) (= (xor (or (=> (not (<= _let_42 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2))) (=> (= (< _let_0 (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) (< _let_46 (ite (< _let_1 _let_2) _let_26 _let_8))) (< _let_34 (ite _let_12 _let_26 v2)))) (< _let_53 (ite (p0 v1 (+ v2 v2)) 1 0))) (= (= (not (<= _let_42 _let_38)) (or (xor (ite (distinct _let_35 _let_11) (< _let_32 _let_51) (p0 (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_5 _let_5) (f1 v1))) (p0 (ite (< _let_1 _let_2) _let_26 _let_8) (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1)))) (or (ite (or (p0 _let_53 (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2))) (distinct (f1 v1) _let_10)) (ite (< _let_43 _let_40) (= (distinct _let_6 _let_6) (>= _let_52 (ite _let_12 _let_26 v2))) (<= _let_26 _let_43)) (and (< _let_33 _let_49) (> _let_6 _let_8))) (=> (p0 _let_47 (ite _let_12 _let_26 v2)) (= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_38))))) (xor (xor (not (distinct _let_54 (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0))) _let_13) (and (=> (=> (not (ite (>= v0 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (distinct (ite _let_18 _let_7 v0) _let_23) (<= (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) _let_0) (<= _let_49 _let_46)) (>= _let_54 _let_51))) (>= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)))) (and (ite (ite (<= _let_27 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (= _let_53 _let_52) (p0 _let_41 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) (< _let_26 _let_22) (ite (>= (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) _let_19) (< (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_21) (p0 _let_23 (ite (< _let_1 _let_2) _let_26 _let_8)))) (ite (distinct _let_45 _let_42) (>= (ite (= _let_3 _let_1) _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_27) _let_16))) (and (= (or (=> (= (> (ite (< _let_1 _let_2) _let_26 _let_8) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9)) (not (not (<= _let_48 _let_48)))) (not (=> (= (< _let_20 _let_0) (xor (= _let_23 _let_2) (xor (distinct _let_40 (ite _let_18 _let_7 v0)) (= _let_7 (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9))))) (and _let_15 (not (distinct _let_25 _let_21)))))) (and (= (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) _let_31) (=> (>= _let_39 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (p0 (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1)) _let_51) (= (p0 _let_39 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) (p0 _let_38 _let_29)) (p0 _let_32 _let_41))))) (xor (>= (+ (+ v2 v2) _let_1) _let_19) (p0 _let_36 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))))) (> _let_35 (ite _let_12 _let_26 v2))))))) (= (or (or (distinct _let_44 _let_24) (= _let_30 (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)))) (ite (p0 _let_31 _let_42) (= (<= _let_20 _let_10) (xor (< _let_48 _let_34) (> _let_3 _let_35))) (>= (ite (< _let_1 _let_2) _let_26 _let_8) _let_38))) (or (<= (+ _let_4 _let_7) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))) (>= _let_37 (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_5 _let_5)))))))))) _let_56 _let_56))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )) diff --git a/test/regress/regress0/uflia/error30.smt b/test/regress/regress0/uflia/error30.smt deleted file mode 100644 index f543cf0e8..000000000 --- a/test/regress/regress0/uflia/error30.smt +++ /dev/null @@ -1,145 +0,0 @@ -(benchmark fuzzsmt -:logic QF_UFLIA -:status sat -:extrafuns ((f0 Int Int Int)) -:extrapreds ((p0 Int Int)) -:extrafuns ((v0 Int)) -:extrafuns ((v1 Int)) -:extrafuns ((v2 Int)) -:formula -(let (?e3 6) -(let (?e4 (f0 v2 v2)) -(let (?e5 (* ?e3 v0)) -(let (?e6 (+ v1 v0)) -(let (?e7 (* v0 ?e3)) -(let (?e8 (* ?e6 (~ ?e3))) -(let (?e9 (* v1 (~ ?e3))) -(let (?e10 (ite (p0 ?e8 v2) 1 0)) -(flet ($e11 (>= ?e7 v2)) -(flet ($e12 (p0 v0 ?e4)) -(flet ($e13 (distinct v2 ?e7)) -(flet ($e14 (> ?e9 ?e6)) -(flet ($e15 (>= ?e9 ?e9)) -(flet ($e16 (< v1 ?e8)) -(flet ($e17 (p0 v1 ?e5)) -(flet ($e18 (> ?e9 v0)) -(flet ($e19 (>= ?e5 ?e7)) -(flet ($e20 (= v1 ?e8)) -(flet ($e21 (p0 ?e5 v0)) -(flet ($e22 (= ?e10 ?e5)) -(let (?e23 (ite $e19 ?e5 v1)) -(let (?e24 (ite $e22 v2 ?e10)) -(let (?e25 (ite $e15 ?e10 ?e24)) -(let (?e26 (ite $e20 ?e4 ?e23)) -(let (?e27 (ite $e16 ?e10 v2)) -(let (?e28 (ite $e17 ?e23 ?e26)) -(let (?e29 (ite $e22 ?e25 ?e26)) -(let (?e30 (ite $e18 ?e10 ?e23)) -(let (?e31 (ite $e11 ?e7 ?e26)) -(let (?e32 (ite $e14 ?e9 ?e27)) -(let (?e33 (ite $e12 ?e8 ?e9)) -(let (?e34 (ite $e13 ?e24 v0)) -(let (?e35 (ite $e21 ?e6 ?e30)) -(flet ($e36 (distinct ?e4 ?e30)) -(flet ($e37 (= ?e8 ?e29)) -(flet ($e38 (p0 ?e6 ?e8)) -(flet ($e39 (p0 ?e7 v0)) -(flet ($e40 (distinct ?e32 ?e5)) -(flet ($e41 (distinct v2 ?e24)) -(flet ($e42 (= v1 ?e29)) -(flet ($e43 (distinct ?e26 ?e26)) -(flet ($e44 (= ?e9 ?e4)) -(flet ($e45 (p0 ?e8 v1)) -(flet ($e46 (= v0 ?e33)) -(flet ($e47 (p0 v0 ?e26)) -(flet ($e48 (distinct ?e32 ?e24)) -(flet ($e49 (= ?e33 ?e29)) -(flet ($e50 (= ?e10 ?e25)) -(flet ($e51 (= v0 ?e30)) -(flet ($e52 (= ?e25 ?e23)) -(flet ($e53 (>= ?e27 ?e31)) -(flet ($e54 (distinct ?e25 ?e25)) -(flet ($e55 (p0 ?e28 ?e30)) -(flet ($e56 (> ?e29 ?e8)) -(flet ($e57 (p0 ?e8 ?e35)) -(flet ($e58 (distinct ?e7 v1)) -(flet ($e59 (distinct ?e7 v1)) -(flet ($e60 (> ?e9 ?e25)) -(flet ($e61 (< ?e33 ?e31)) -(flet ($e62 (< ?e4 ?e6)) -(flet ($e63 (< ?e35 ?e27)) -(flet ($e64 (<= ?e28 ?e23)) -(flet ($e65 (<= ?e8 ?e26)) -(flet ($e66 (<= ?e28 ?e29)) -(flet ($e67 (p0 ?e9 ?e29)) -(flet ($e68 (p0 ?e4 ?e24)) -(flet ($e69 (< ?e24 ?e25)) -(flet ($e70 (= ?e31 ?e7)) -(flet ($e71 (p0 ?e31 ?e10)) -(flet ($e72 (>= ?e28 ?e24)) -(flet ($e73 (< ?e34 ?e31)) -(flet ($e74 (implies $e53 $e22)) -(flet ($e75 (iff $e41 $e55)) -(flet ($e76 (if_then_else $e40 $e20 $e51)) -(flet ($e77 (xor $e75 $e12)) -(flet ($e78 (not $e39)) -(flet ($e79 (iff $e69 $e70)) -(flet ($e80 (or $e21 $e17)) -(flet ($e81 (not $e11)) -(flet ($e82 (if_then_else $e77 $e56 $e79)) -(flet ($e83 (implies $e64 $e38)) -(flet ($e84 (xor $e13 $e74)) -(flet ($e85 (implies $e67 $e68)) -(flet ($e86 (not $e66)) -(flet ($e87 (xor $e19 $e85)) -(flet ($e88 (not $e49)) -(flet ($e89 (iff $e72 $e15)) -(flet ($e90 (not $e16)) -(flet ($e91 (and $e48 $e63)) -(flet ($e92 (iff $e65 $e89)) -(flet ($e93 (xor $e81 $e91)) -(flet ($e94 (implies $e73 $e60)) -(flet ($e95 (iff $e45 $e44)) -(flet ($e96 (xor $e52 $e84)) -(flet ($e97 (not $e43)) -(flet ($e98 (if_then_else $e42 $e96 $e86)) -(flet ($e99 (or $e82 $e57)) -(flet ($e100 (iff $e92 $e47)) -(flet ($e101 (if_then_else $e83 $e83 $e14)) -(flet ($e102 (xor $e95 $e99)) -(flet ($e103 (xor $e58 $e50)) -(flet ($e104 (implies $e36 $e88)) -(flet ($e105 (implies $e18 $e71)) -(flet ($e106 (if_then_else $e59 $e37 $e78)) -(flet ($e107 (xor $e106 $e93)) -(flet ($e108 (iff $e80 $e105)) -(flet ($e109 (not $e100)) -(flet ($e110 (and $e107 $e54)) -(flet ($e111 (if_then_else $e61 $e61 $e76)) -(flet ($e112 (if_then_else $e98 $e108 $e108)) -(flet ($e113 (iff $e112 $e104)) -(flet ($e114 (if_then_else $e46 $e46 $e110)) -(flet ($e115 (not $e90)) -(flet ($e116 (iff $e62 $e114)) -(flet ($e117 (if_then_else $e97 $e115 $e97)) -(flet ($e118 (iff $e117 $e101)) -(flet ($e119 (and $e109 $e109)) -(flet ($e120 (and $e111 $e111)) -(flet ($e121 (xor $e119 $e94)) -(flet ($e122 (xor $e118 $e102)) -(flet ($e123 (implies $e87 $e120)) -(flet ($e124 (xor $e103 $e123)) -(flet ($e125 (implies $e121 $e121)) -(flet ($e126 (or $e113 $e113)) -(flet ($e127 (not $e126)) -(flet ($e128 (if_then_else $e125 $e116 $e127)) -(flet ($e129 (iff $e122 $e128)) -(flet ($e130 (or $e124 $e124)) -(flet ($e131 (or $e130 $e130)) -(flet ($e132 (implies $e129 $e129)) -(flet ($e133 (or $e131 $e131)) -(flet ($e134 (not $e133)) -(flet ($e135 (implies $e132 $e134)) -$e135 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - diff --git a/test/regress/regress0/uflia/error30.smtv1.smt2 b/test/regress/regress0/uflia/error30.smtv1.smt2 new file mode 100644 index 000000000..f2e6d5692 --- /dev/null +++ b/test/regress/regress0/uflia/error30.smtv1.smt2 @@ -0,0 +1,9 @@ +(set-option :incremental false) +(set-info :status sat) +(set-logic QF_UFLIA) +(declare-fun f0 (Int Int) Int) +(declare-fun p0 (Int Int) Bool) +(declare-fun v0 () Int) +(declare-fun v1 () Int) +(declare-fun v2 () Int) +(check-sat-assuming ( (let ((_let_0 (f0 v2 v2))) (let ((_let_1 (* 6 v0))) (let ((_let_2 (* (+ v1 v0) (- 6)))) (let ((_let_3 (* v1 (- 6)))) (let ((_let_4 (ite (p0 _let_2 v2) 1 0))) (let ((_let_5 (= v1 _let_2))) (let ((_let_6 (ite (>= _let_1 (* v0 6)) _let_1 v1))) (let ((_let_7 (ite (= _let_4 _let_1) v2 _let_4))) (let ((_let_8 (ite (>= _let_3 _let_3) _let_4 _let_7))) (let ((_let_9 (ite (p0 _let_1 v0) (+ v1 v0) (ite (> _let_3 v0) _let_4 _let_6)))) (let ((_let_10 (= (xor (= (ite (not (distinct (ite _let_5 _let_0 _let_6) (ite _let_5 _let_0 _let_6))) (not (not (< v1 _let_2))) (not (distinct (ite _let_5 _let_0 _let_6) (ite _let_5 _let_0 _let_6)))) (ite (=> (<= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) _let_6) (p0 (+ v1 v0) _let_2)) (=> (<= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) _let_6) (p0 (+ v1 v0) _let_2)) (> _let_3 (+ v1 v0)))) (xor (= (p0 _let_2 v1) (= _let_3 _let_0)) (or (ite (xor (= (distinct v2 _let_7) (p0 (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) (ite (> _let_3 v0) _let_4 _let_6))) (p0 v0 _let_0)) (> (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6)) _let_2) (= (< _let_7 _let_8) (= (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6)) (* v0 6)))) (p0 _let_2 _let_9)))) (ite (=> (xor (and (not (= (= (<= _let_2 (ite _let_5 _let_0 _let_6)) (= (>= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) _let_7) (>= _let_3 _let_3))) (p0 v0 (ite _let_5 _let_0 _let_6)))) (not (= (= (<= _let_2 (ite _let_5 _let_0 _let_6)) (= (>= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) _let_7) (>= _let_3 _let_3))) (p0 v0 (ite _let_5 _let_0 _let_6))))) (=> (< (ite (distinct v2 (* v0 6)) _let_7 v0) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (> _let_3 _let_8))) (xor (and (not (= (= (<= _let_2 (ite _let_5 _let_0 _let_6)) (= (>= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) _let_7) (>= _let_3 _let_3))) (p0 v0 (ite _let_5 _let_0 _let_6)))) (not (= (= (<= _let_2 (ite _let_5 _let_0 _let_6)) (= (>= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) _let_7) (>= _let_3 _let_3))) (p0 v0 (ite _let_5 _let_0 _let_6))))) (=> (< (ite (distinct v2 (* v0 6)) _let_7 v0) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (> _let_3 _let_8)))) (= (< _let_0 (+ v1 v0)) (ite (= v0 (ite (p0 v0 _let_0) _let_2 _let_3)) (= v0 (ite (p0 v0 _let_0) _let_2 _let_3)) (and (xor (ite (distinct (* v0 6) v1) (= _let_2 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (not (p0 (* v0 6) v0))) (xor (not (>= (* v0 6) v2)) (and (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_7) (< _let_9 (ite (< v1 _let_2) _let_4 v2))))) (distinct _let_8 _let_8)))) (not (or (= (ite (ite (= v1 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (xor (= _let_8 _let_6) (xor (distinct v2 (* v0 6)) (=> (>= (ite (< v1 _let_2) _let_4 v2) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (= _let_4 _let_1)))) (not (<= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))))) (= (or (p0 _let_1 v0) (p0 v1 _let_1)) (=> (> _let_3 v0) (p0 (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6)) _let_4))) (= (or (p0 _let_1 v0) (p0 v1 _let_1)) (=> (> _let_3 v0) (p0 (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6)) _let_4)))) (=> (distinct _let_0 (ite (> _let_3 v0) _let_4 _let_6)) (not (= (ite (p0 v0 _let_0) _let_2 _let_3) (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6)))))) (= (ite (ite (= v1 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (xor (= _let_8 _let_6) (xor (distinct v2 (* v0 6)) (=> (>= (ite (< v1 _let_2) _let_4 v2) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (= _let_4 _let_1)))) (not (<= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))))) (= (or (p0 _let_1 v0) (p0 v1 _let_1)) (=> (> _let_3 v0) (p0 (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6)) _let_4))) (= (or (p0 _let_1 v0) (p0 v1 _let_1)) (=> (> _let_3 v0) (p0 (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6)) _let_4)))) (=> (distinct _let_0 (ite (> _let_3 v0) _let_4 _let_6)) (not (= (ite (p0 v0 _let_0) _let_2 _let_3) (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6)))))))))))) (let ((_let_11 (or (or (xor (xor (distinct (* v0 6) v1) (= _let_4 _let_8)) (=> (xor (>= _let_1 (* v0 6)) (=> (p0 _let_3 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (p0 _let_0 _let_7))) (and (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6)))) (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6))))))) (xor (xor (distinct (* v0 6) v1) (= _let_4 _let_8)) (=> (xor (>= _let_1 (* v0 6)) (=> (p0 _let_3 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (p0 _let_0 _let_7))) (and (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6)))) (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6)))))))) (or (xor (xor (distinct (* v0 6) v1) (= _let_4 _let_8)) (=> (xor (>= _let_1 (* v0 6)) (=> (p0 _let_3 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (p0 _let_0 _let_7))) (and (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6)))) (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6))))))) (xor (xor (distinct (* v0 6) v1) (= _let_4 _let_8)) (=> (xor (>= _let_1 (* v0 6)) (=> (p0 _let_3 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (p0 _let_0 _let_7))) (and (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6)))) (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6))))))))))) (=> (=> _let_10 _let_10) (not (or _let_11 _let_11))))))))))))))) )) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt deleted file mode 100644 index c7fed0c15..000000000 --- a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt +++ /dev/null @@ -1,48 +0,0 @@ -(benchmark mathsat -:logic QF_UFLIA -:extrafuns ((s_count Int Int)) -:extrafuns ((fmt1 Int)) -:extrafuns ((fmt_length Int)) -:status unsat -:formula -(let (?n1 0) -(let (?n2 6) -(let (?n3 (s_count ?n2)) -(flet ($n4 (= ?n1 ?n3)) -(let (?n5 5) -(let (?n6 (s_count ?n5)) -(flet ($n7 (= ?n1 ?n6)) -(let (?n8 4) -(let (?n9 (s_count ?n8)) -(flet ($n10 (= ?n1 ?n9)) -(let (?n11 3) -(let (?n12 (s_count ?n11)) -(flet ($n13 (= ?n1 ?n12)) -(let (?n14 1) -(let (?n15 (s_count ?n1)) -(flet ($n16 (= ?n14 ?n15)) -(let (?n17 (s_count ?n14)) -(flet ($n18 (= ?n1 ?n17)) -(flet ($n19 (and $n16 $n18)) -(let (?n20 2) -(let (?n21 (s_count ?n20)) -(flet ($n22 (= ?n1 ?n21)) -(flet ($n23 (and $n19 $n22)) -(flet ($n24 (and $n13 $n23)) -(flet ($n25 (and $n10 $n24)) -(flet ($n26 (and $n7 $n25)) -(flet ($n27 (and $n4 $n26)) -(let (?n28 9) -(flet ($n29 (= ?n28 fmt_length)) -(flet ($n30 (> fmt1 ?n14)) -(flet ($n31 (< fmt1 fmt_length)) -(flet ($n32 (and $n30 $n31)) -(let (?n33 (- fmt1 ?n20)) -(let (?n34 (s_count ?n33)) -(let (?n35 (+ ?n14 ?n34)) -(flet ($n36 (= ?n1 ?n35)) -(flet ($n37 (and $n32 $n36)) -(flet ($n38 (and $n29 $n37)) -(flet ($n39 (and $n27 $n38)) -$n39 -)))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smtv1.smt2 b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smtv1.smt2 new file mode 100644 index 000000000..e6405f0eb --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smtv1.smt2 @@ -0,0 +1,7 @@ +(set-option :incremental false) +(set-info :status unsat) +(set-logic QF_UFLIA) +(declare-fun s_count (Int) Int) +(declare-fun fmt1 () Int) +(declare-fun fmt_length () Int) +(check-sat-assuming ( (and (and (= 0 (s_count 6)) (and (= 0 (s_count 5)) (and (= 0 (s_count 4)) (and (= 0 (s_count 3)) (and (and (= 1 (s_count 0)) (= 0 (s_count 1))) (= 0 (s_count 2))))))) (and (= 9 fmt_length) (and (and (> fmt1 1) (< fmt1 fmt_length)) (= 0 (+ 1 (s_count (- fmt1 2))))))) )) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt deleted file mode 100644 index fb16651ff..000000000 --- a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt +++ /dev/null @@ -1,40 +0,0 @@ -(benchmark mathsat -:logic QF_UFLIA -:extrafuns ((arg1 Int)) -:extrafuns ((adr_lo Int)) -:extrafuns ((select_format Int Int)) -:extrafuns ((x Int)) -:status sat -:formula -(let (?n1 (select_format arg1)) -(flet ($n2 (= ?n1 adr_lo)) -(let (?n3 0) -(flet ($n4 (= ?n3 x)) -(let (?n5 4) -(let (?n6 (select_format ?n5)) -(flet ($n7 (= adr_lo ?n6)) -(let (?n8 3) -(let (?n9 (select_format ?n8)) -(flet ($n10 (= adr_lo ?n9)) -(let (?n11 2) -(let (?n12 (select_format ?n11)) -(flet ($n13 (= adr_lo ?n12)) -(let (?n14 1) -(let (?n15 (select_format ?n3)) -(flet ($n16 (= ?n14 ?n15)) -(let (?n17 (select_format ?n14)) -(flet ($n18 (= ?n3 ?n17)) -(flet ($n19 (or $n16 $n18)) -(flet ($n20 (or $n13 $n19)) -(flet ($n21 (or $n10 $n20)) -(flet ($n22 (or $n7 $n21)) -(flet ($n23 (or $n4 $n22)) -(flet ($n24 (= adr_lo ?n8)) -(flet ($n25 (< arg1 ?n5)) -(flet ($n26 (>= arg1 ?n3)) -(flet ($n27 (and $n25 $n26)) -(flet ($n28 (and $n24 $n27)) -(flet ($n29 (and $n23 $n28)) -(flet ($n30 (and $n2 $n29)) -$n30 -))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smtv1.smt2 b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smtv1.smt2 new file mode 100644 index 000000000..21e26dac9 --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smtv1.smt2 @@ -0,0 +1,8 @@ +(set-option :incremental false) +(set-info :status sat) +(set-logic QF_UFLIA) +(declare-fun arg1 () Int) +(declare-fun adr_lo () Int) +(declare-fun select_format (Int) Int) +(declare-fun x () Int) +(check-sat-assuming ( (and (= (select_format arg1) adr_lo) (and (or (= 0 x) (or (= adr_lo (select_format 4)) (or (= adr_lo (select_format 3)) (or (= adr_lo (select_format 2)) (or (= 1 (select_format 0)) (= 0 (select_format 1))))))) (and (= adr_lo 3) (and (< arg1 4) (>= arg1 0))))) )) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt deleted file mode 100644 index 6f65e83ec..000000000 --- a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt +++ /dev/null @@ -1,45 +0,0 @@ -(benchmark mathsat -:logic QF_UFLIA -:extrafuns ((fmt_length Int)) -:extrafuns ((fmt1 Int)) -:extrafuns ((arg1 Int)) -:extrafuns ((select_format Int Int)) -:status sat -:formula -(let (?n1 1) -(let (?n2 (+ ?n1 fmt1)) -(let (?n3 (select_format ?n2)) -(flet ($n4 (= ?n1 ?n3)) -(let (?n5 (select_format arg1)) -(let (?n6 0) -(flet ($n7 (= ?n5 ?n6)) -(flet ($n8 (and $n4 $n7)) -(let (?n9 7) -(let (?n10 (select_format ?n9)) -(flet ($n11 (= ?n1 ?n10)) -(let (?n12 (select_format ?n6)) -(flet ($n13 (= ?n1 ?n12)) -(let (?n14 (select_format ?n1)) -(flet ($n15 (= ?n1 ?n14)) -(flet ($n16 (or $n13 $n15)) -(let (?n17 5) -(let (?n18 (select_format ?n17)) -(flet ($n19 (= ?n6 ?n18)) -(flet ($n20 (or $n16 $n19)) -(let (?n21 6) -(let (?n22 (select_format ?n21)) -(flet ($n23 (= ?n6 ?n22)) -(flet ($n24 (or $n20 $n23)) -(flet ($n25 (or $n11 $n24)) -(let (?n26 9) -(flet ($n27 (= ?n26 fmt_length)) -(let (?n28 2) -(let (?n29 (- fmt1 ?n28)) -(flet ($n30 (= arg1 ?n29)) -(flet ($n31 (< fmt1 fmt_length)) -(flet ($n32 (and $n30 $n31)) -(flet ($n33 (and $n27 $n32)) -(flet ($n34 (and $n25 $n33)) -(flet ($n35 (and $n8 $n34)) -$n35 -)))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smtv1.smt2 b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smtv1.smt2 new file mode 100644 index 000000000..3ba9bf6ce --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smtv1.smt2 @@ -0,0 +1,8 @@ +(set-option :incremental false) +(set-info :status sat) +(set-logic QF_UFLIA) +(declare-fun fmt_length () Int) +(declare-fun fmt1 () Int) +(declare-fun arg1 () Int) +(declare-fun select_format (Int) Int) +(check-sat-assuming ( (and (and (= 1 (select_format (+ 1 fmt1))) (= (select_format arg1) 0)) (and (or (= 1 (select_format 7)) (or (or (or (= 1 (select_format 0)) (= 1 (select_format 1))) (= 0 (select_format 5))) (= 0 (select_format 6)))) (and (= 9 fmt_length) (and (= arg1 (- fmt1 2)) (< fmt1 fmt_length))))) )) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt deleted file mode 100644 index f1212a876..000000000 --- a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt +++ /dev/null @@ -1,67 +0,0 @@ -(benchmark mathsat -:logic QF_UFLIA -:extrafuns ((fmt_length Int)) -:extrafuns ((fmt1 Int)) -:extrafuns ((x_count Int Int)) -:extrafuns ((select_format Int Int)) -:extrafuns ((percent Int)) -:extrafuns ((s_count Int Int)) -:status sat -:formula -(let (?n1 1) -(let (?n2 5) -(let (?n3 (x_count ?n2)) -(flet ($n4 (= ?n1 ?n3)) -(let (?n5 4) -(let (?n6 (x_count ?n5)) -(flet ($n7 (= ?n1 ?n6)) -(let (?n8 3) -(let (?n9 (x_count ?n8)) -(let (?n10 2) -(let (?n11 (x_count ?n10)) -(flet ($n12 (= ?n9 ?n11)) -(let (?n13 0) -(let (?n14 (select_format ?n8)) -(flet ($n15 (= ?n13 ?n14)) -(let (?n16 (x_count ?n13)) -(flet ($n17 (= ?n1 ?n16)) -(flet ($n18 (= ?n1 percent)) -(flet ($n19 true) -(let (?n20 (s_count ?n13)) -(flet ($n21 (= ?n13 ?n20)) -(flet ($n22 (if_then_else $n18 $n19 $n21)) -(let (?n23 (select_format ?n10)) -(flet ($n24 (= percent ?n23)) -(flet ($n25 (= ?n1 ?n14)) -(flet ($n26 (and $n24 $n25)) -(flet ($n27 false) -(flet ($n28 (if_then_else $n26 $n27 $n19)) -(flet ($n29 (and $n22 $n28)) -(flet ($n30 (and $n17 $n29)) -(flet ($n31 (= ?n13 percent)) -(flet ($n32 (= ?n13 ?n23)) -(flet ($n33 (and $n31 $n32)) -(let (?n34 (x_count ?n1)) -(flet ($n35 (= ?n13 ?n34)) -(flet ($n36 (= ?n16 ?n34)) -(flet ($n37 (if_then_else $n33 $n35 $n36)) -(flet ($n38 (and $n30 $n37)) -(flet ($n39 (and $n15 $n38)) -(flet ($n40 (and $n12 $n39)) -(flet ($n41 (and $n7 $n40)) -(flet ($n42 (and $n4 $n41)) -(let (?n43 9) -(flet ($n44 (= ?n43 fmt_length)) -(let (?n45 (- fmt1 ?n10)) -(let (?n46 (x_count ?n45)) -(let (?n47 (+ ?n1 ?n46)) -(flet ($n48 (= ?n13 ?n47)) -(flet ($n49 (> fmt1 ?n1)) -(let (?n50 (- fmt_length ?n1)) -(flet ($n51 (< fmt1 ?n50)) -(flet ($n52 (and $n49 $n51)) -(flet ($n53 (and $n48 $n52)) -(flet ($n54 (and $n44 $n53)) -(flet ($n55 (and $n42 $n54)) -$n55 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smtv1.smt2 b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smtv1.smt2 new file mode 100644 index 000000000..4c8aca492 --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smtv1.smt2 @@ -0,0 +1,10 @@ +(set-option :incremental false) +(set-info :status sat) +(set-logic QF_UFLIA) +(declare-fun fmt_length () Int) +(declare-fun fmt1 () Int) +(declare-fun x_count (Int) Int) +(declare-fun select_format (Int) Int) +(declare-fun percent () Int) +(declare-fun s_count (Int) Int) +(check-sat-assuming ( (let ((_let_0 (select_format 3))) (let ((_let_1 (x_count 0))) (let ((_let_2 (select_format 2))) (let ((_let_3 (x_count 1))) (and (and (= 1 (x_count 5)) (and (= 1 (x_count 4)) (and (= (x_count 3) (x_count 2)) (and (= 0 _let_0) (and (and (= 1 _let_1) (and (ite (= 1 percent) true (= 0 (s_count 0))) (ite (and (= percent _let_2) (= 1 _let_0)) false true))) (ite (and (= 0 percent) (= 0 _let_2)) (= 0 _let_3) (= _let_1 _let_3))))))) (and (= 9 fmt_length) (and (= 0 (+ 1 (x_count (- fmt1 2)))) (and (> fmt1 1) (< fmt1 (- fmt_length 1)))))))))) )) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smt deleted file mode 100644 index 23e4ba01f..000000000 --- a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smt +++ /dev/null @@ -1,18 +0,0 @@ -(benchmark mathsat -:logic QF_UFLIA -:extrafuns ((select_format Int Int)) -:extrafuns ((adr_lo Int)) -:extrafuns ((arg1 Int)) -:status unknown -:formula -(let (?n1 (select_format arg1)) -(flet ($n2 (= ?n1 adr_lo)) -(let (?n3 0) -(flet ($n4 (= adr_lo ?n3)) -(let (?n5 1) -(let (?n6 (select_format ?n5)) -(flet ($n7 (= adr_lo ?n6)) -(flet ($n8 (or $n4 $n7)) -(flet ($n9 (and $n2 $n8)) -$n9 -)))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2 b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2 new file mode 100644 index 000000000..e8386d2ab --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2 @@ -0,0 +1,7 @@ +(set-option :incremental false) +(set-info :status unknown) +(set-logic QF_UFLIA) +(declare-fun select_format (Int) Int) +(declare-fun adr_lo () Int) +(declare-fun arg1 () Int) +(check-sat-assuming ( (and (= (select_format arg1) adr_lo) (or (= adr_lo 0) (= adr_lo (select_format 1)))) )) |