Add regressions for fixed issue (#8237)

Adds regressions for an issue that has been fixed in the meantime.
Fixes #4334

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 50969c740b727a50079ba8a3bd709c7d1faaed6c..8d50b53f773a1bbf1d547f8efba1dc7c549cc517 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -772,6 +772,7 @@ set(regress_0_tests
   regress0/nl/issue3971.smt2
   regress0/nl/issue3991.smt2
   regress0/nl/issue4007-rint-uf.smt2
+  regress0/nl/issue4334-sat-proof-min.smt2
   regress0/nl/issue4463-ack-model.smt2
   regress0/nl/issue5534-no-assertions.smt2
   regress0/nl/issue5726-downpolys.smt2
@@ -1933,6 +1934,7 @@ set(regress_1_tests
   regress1/nl/issue3803-nl-check-model.smt2
   regress1/nl/issue3955-ee-double-notify.smt2
   regress1/nl/issue3966-conf-coeff.smt2
+  regress1/nl/issue4334-sat-proof.smt2
   regress1/nl/issue4791-llr.smt2
   regress1/nl/issue5372-2-no-m-presolve.smt2
   regress1/nl/issue5461-iand-init-refine.smt2

diff --git a/test/regress/regress0/nl/issue4334-sat-proof-min.smt2 b/test/regress/regress0/nl/issue4334-sat-proof-min.smt2
new file mode 100644 (file)
index 0000000..3b58178
--- /dev/null
+++ b/test/regress/regress0/nl/issue4334-sat-proof-min.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: -i -q
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-option :produce-unsat-cores true)
+(assert (distinct 0 (mod 0 0)))
+(check-sat)
+(check-sat)
+(check-sat)
+(check-sat)
\ No newline at end of file

diff --git a/test/regress/regress1/nl/issue4334-sat-proof.smt2 b/test/regress/regress1/nl/issue4334-sat-proof.smt2
new file mode 100644 (file)
index 0000000..b8ea48b
--- /dev/null
+++ b/test/regress/regress1/nl/issue4334-sat-proof.smt2
@@ -0,0 +1,241 @@
+; COMMAND-LINE: -i --produce-unsat-cores --nl-ext-purify
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_NIA)
+(set-option :produce-unsat-cores true)
+(set-option :nl-ext-purify true)
+(declare-const v0 Bool)
+(declare-const v1 Bool)
+(declare-const v2 Bool)
+(declare-const v3 Bool)
+(declare-const v4 Bool)
+(declare-const v5 Bool)
+(declare-const v6 Bool)
+(declare-const v7 Bool)
+(declare-const v8 Bool)
+(declare-const v9 Bool)
+(declare-const v10 Bool)
+(declare-const v11 Bool)
+(declare-const v12 Bool)
+(declare-const v13 Bool)
+(declare-const v14 Bool)
+(declare-const i0 Int)
+(push 1)
+(pop 1)
+(declare-const v15 Bool)
+(declare-const i1 Int)
+(declare-const i2 Int)
+(declare-const v16 Bool)
+(push 1)
+(declare-const v17 Bool)
+(push 1)
+(declare-const v18 Bool)
+(declare-const v19 Bool)
+(declare-const v20 Bool)
+(push 1)
+(declare-const v21 Bool)
+(declare-const i3 Int)
+(declare-const v22 Bool)
+(declare-const v23 Bool)
+(declare-const v24 Bool)
+(declare-const v25 Bool)
+(declare-const i4 Int)
+(pop 1)
+(declare-const i5 Int)
+(declare-const v26 Bool)
+(declare-const i6 Int)
+(declare-const v27 Bool)
+(declare-const v28 Bool)
+(pop 1)
+(declare-const v29 Bool)
+(declare-const i7 Int)
+(declare-const v30 Bool)
+(declare-const v31 Bool)
+(declare-const v32 Bool)
+(declare-const v33 Bool)
+(pop 1)
+(declare-const v34 Bool)
+(declare-const v35 Bool)
+(declare-const v36 Bool)
+(declare-const v37 Bool)
+(declare-const i8 Int)
+(declare-const v38 Bool)
+(push 1)
+(declare-const v39 Bool)
+(pop 1)
+(declare-const v40 Bool)
+(push 1)
+(pop 1)
+(declare-const v41 Bool)
+(declare-const v42 Bool)
+(declare-const i9 Int)
+(declare-const v43 Bool)
+(declare-const v44 Bool)
+(push 1)
+(push 1)
+(declare-const v45 Bool)
+(push 1)
+(push 1)
+(declare-const v46 Bool)
+(declare-const v47 Bool)
+(declare-const i10 Int)
+(declare-const v48 Bool)
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855) (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4) v16 v11) :named IP_1))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4)) :named IP_2))
+(assert (! (or v16) :named IP_3))
+(assert (! (or v45 (and v9 v4) v16 (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855) v11 v16 v45 (and v9 v4) v45 v11 (and v9 v4) (<= (abs 814) 855)) :named IP_4))
+(assert (! (or v45 (and v9 v4) (and v9 v4)) :named IP_5))
+(assert (! (or v45) :named IP_6))
+(assert (! (or (and v9 v4)) :named IP_7))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4)) :named IP_8))
+(assert (! (or (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_9))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_10))
+(assert (! (or (and v9 v4) v11) :named IP_11))
+(assert (! (or (and v9 v4) v11 v16 v45) :named IP_12))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_13))
+(assert (! (or v11 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_14))
+(assert (! (or (<= (abs 814) 855)) :named IP_15))
+(assert (! (or v11 (<= (abs 814) 855) (<= (abs 814) 855)) :named IP_16))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_17))
+(assert (! (or v11 v11) :named IP_18))
+(assert (! (or v45 v16 (and v9 v4) (and v9 v4) (and v9 v4) v16) :named IP_19))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_20))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v11) :named IP_21))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_22))
+(assert (! (or v16 (and v9 v4) v11 (and v9 v4) v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4) v16 v45) :named IP_23))
+(assert (! (or (and v9 v4) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v16 v45) :named IP_24))
+(assert (! (or v11 v45 v11 v45) :named IP_25))
+(assert (! (or v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v11 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855)) :named IP_26))
+(assert (! (or (and v9 v4) (<= (abs 814) 855) (and v9 v4) (<= (abs 814) 855) (<= (abs 814) 855) v45) :named IP_27))
+(assert (! (or v16 v11) :named IP_28))
+(assert (! (or v11 v16) :named IP_29))
+(assert (! (or v11 v11) :named IP_30))
+(assert (! (or v11 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) (<= (abs 814) 855) (<= (abs 814) 855)) :named IP_31))
+(assert (! (or (and v9 v4)) :named IP_32))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_33))
+(assert (! (or (and v9 v4)) :named IP_34))
+(assert (! (or v11 v11 v16) :named IP_35))
+(assert (! (or v45 (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855)) :named IP_36))
+(assert (! (or v11 v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4) v16 (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_37))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_38))
+(assert (! (or v16 v45) :named IP_39))
+(assert (! (or v16 (and v9 v4)) :named IP_40))
+(assert (! (or v45 v45) :named IP_41))
+(assert (! (or v16 v45 v45 v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v16) :named IP_42))
+(assert (! (or (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_43))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v16 v11) :named IP_44))
+(assert (! (or (<= (abs 814) 855)) :named IP_45))
+(assert (! (or v45 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_46))
+(assert (! (or (and v9 v4) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v45 v45) :named IP_47))
+(assert (! (or (and v9 v4) v11) :named IP_48))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v11 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v16) :named IP_49))
+(assert (! (or (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4)) :named IP_50))
+(assert (! (or (and v9 v4) (and v9 v4)) :named IP_51))
+(assert (! (or v45 (<= (abs 814) 855) v11) :named IP_52))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) (<= (abs 814) 855)) :named IP_53))
+(assert (! (or (and v9 v4) v16 v11 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v45 (<= (abs 814) 855) v45) :named IP_54))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v16 v45) :named IP_55))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4)) :named IP_56))
+(assert (! (or (and v9 v4) (<= (abs 814) 855)) :named IP_57))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_58))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v45 (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_59))
+(assert (! (or v16 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855) v11 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_60))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) v16 (and v9 v4) v45 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v16 (<= (abs 814) 855) v16 (<= (abs 814) 855) v45) :named IP_61))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_62))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855) (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_63))
+(assert (! (or v45) :named IP_64))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v11 v16) :named IP_65))
+(assert (! (or (and v9 v4) (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_66))
+(assert (! (or v45 v45) :named IP_67))
+(assert (! (or (and v9 v4) v16 v11 (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4)) :named IP_68))
+(assert (! (or (and v9 v4)) :named IP_69))
+(assert (! (or v16 (<= (abs 814) 855) v45 v16) :named IP_70))
+(assert (! (or v11 v45 v16 (and v9 v4)) :named IP_71))
+(assert (! (or (and v9 v4) (and v9 v4)) :named IP_72))
+(assert (! (or (<= (abs 814) 855) (<= (abs 814) 855)) :named IP_73))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v11) :named IP_74))
+(assert (! (or (<= (abs 814) 855) v16 v11) :named IP_75))
+(assert (! (or (<= (abs 814) 855) (<= (abs 814) 855)) :named IP_76))
+(assert (! (or v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4) (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855)) :named IP_77))
+(assert (! (or v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v45) :named IP_78))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4)) :named IP_79))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_80))
+(assert (! (or (<= (abs 814) 855)) :named IP_81))
+(assert (! (or v45 v11 (and v9 v4)) :named IP_82))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v16 v45 v16) :named IP_83))
+(assert (! (or (and v9 v4)) :named IP_84))
+(assert (! (or (<= (abs 814) 855) v11 v11 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_85))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_86))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v16) :named IP_87))
+(assert (! (or v45 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_88))
+(assert (! (or (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v16 v16) :named IP_89))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v11 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_90))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_91))
+(assert (! (or v45 v45 v16) :named IP_92))
+(assert (! (or v16) :named IP_93))
+(assert (! (or (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v45 (<= (abs 814) 855) v45 (<= (abs 814) 855)) :named IP_94))
+(assert (! (or v45 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_95))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_96))
+(assert (! (or (and v9 v4)) :named IP_97))
+(assert (! (or v11) :named IP_98))
+(assert (! (or v45 (<= (abs 814) 855) (and v9 v4) (<= (abs 814) 855) v16 v45) :named IP_99))
+(assert (! (or (and v9 v4) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855)) :named IP_100))
+(assert (! (or (<= (abs 814) 855) (<= (abs 814) 855) (<= (abs 814) 855) v16 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_101))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_102))
+(assert (! (or v11 (and v9 v4)) :named IP_103))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_104))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_105))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v45 v16 (<= (abs 814) 855)) :named IP_106))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4) (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_107))
+(assert (! (or v45 v11 (and v9 v4) v45) :named IP_108))
+(assert (! (or v16) :named IP_109))
+(assert (! (or (and v9 v4) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_110))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v45 v16 v11 v45 (and v9 v4)) :named IP_111))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_112))
+(assert (! (or v11 (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_113))
+(assert (! (or v11) :named IP_114))
+(assert (! (or (<= (abs 814) 855)) :named IP_115))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_116))
+(assert (! (or v45) :named IP_117))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) v11 (and v9 v4)) :named IP_118))
+(assert (! (or v16) :named IP_119))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_120))
+(assert (! (or v11 (and v9 v4) v11 (<= (abs 814) 855) v16 v45 (<= (abs 814) 855) v16 (and v9 v4) v16 v45 (<= (abs 814) 855) v16) :named IP_121))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_122))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_123))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_124))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_125))
+(assert (! (or v11 v11 v16) :named IP_126))
+(assert (! (or (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855) (<= (abs 814) 855)) :named IP_127))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v45) :named IP_128))
+(assert (! (or v45 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v16) :named IP_129))
+(assert (! (or v16 v11 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_130))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_131))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_132))
+(assert (! (or (<= (abs 814) 855)) :named IP_133))
+(assert (! (or v11) :named IP_134))
+(assert (! (or (<= (abs 814) 855) v45) :named IP_135))
+(assert (! (or v16 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_136))
+(assert (! (or (<= (abs 814) 855) v16 v11) :named IP_137))
+(assert (! (or v45 (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4)) :named IP_138))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_139))
+(assert (! (or v45) :named IP_140))
+(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_141))
+(assert (! (or v16 v45 (<= (abs 814) 855)) :named IP_142))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v45 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v16) :named IP_143))
+(assert (! (or v11 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) v11) :named IP_144))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_145))
+(assert (! (or v11) :named IP_146))
+(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4) (and v9 v4)) :named IP_147))
+(assert (! (or v11 v45 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4)) :named IP_148))
+(assert (! (or v11) :named IP_149))
+(assert (! (or (and v9 v4) (<= (abs 814) 855)) :named IP_150))
+(assert (! (or v16 v16) :named IP_151))
+(assert (! (or v45 v16) :named IP_152))
+(check-sat)
+(check-sat-assuming (IP_144 IP_147))
+(check-sat-assuming (IP_35 IP_87))
+(check-sat-assuming (IP_55 IP_106))
+(exit)