OK

UnitTests/sat/QF_ABV/try5_small_noof_functions_wp_fmt.set_other_indent.il.wp.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_ABV)
-(set-info :source |
-Ivan Jager <aij+nospam@andrew.cmu.edu>
-
-|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun mem_35_142 () (Array (_ BitVec 32) (_ BitVec 8)))
-(declare-fun R_EAX_5_89 () (_ BitVec 32))
-(declare-fun R_EBP_0_70 () (_ BitVec 32))
-(declare-fun R_ESP_1_58 () (_ BitVec 32))
-(assert (let ((?v_0 (concat (_ bv0 24) (select mem_35_142 (_ bv134534658 32))))) (let ((?v_1 (bvand (bvsub ?v_0 (_ bv0 32)) (_ bv255 32))) (?v_2 (bvsub R_ESP_1_58 (_ bv4 32)))) (let ((?v_5 (store (store (store (store mem_35_142 (bvadd ?v_2 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBP_0_70 (_ bv24 32)))) (bvadd ?v_2 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBP_0_70 (_ bv16 32)))) (bvadd ?v_2 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBP_0_70 (_ bv8 32)))) (bvadd ?v_2 (_ bv0 32)) ((_ extract 7 0) R_EBP_0_70))) (?v_24 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_1 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))))) (let ((?v_3 (concat (_ bv0 24) (select ?v_5 (_ bv134534656 32))))) (let ((?v_4 (bvand (bvsub ?v_3 (_ bv0 32)) (_ bv255 32)))) (let ((?v_22 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_4 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))) (?v_6 (concat (_ bv0 24) (select ?v_5 (_ bv134534657 32))))) (let ((?v_7 (bvand (bvsub ?v_6 (_ bv0 32)) (_ bv255 32)))) (let ((?v_8 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_7 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))) (?v_15 (bvnot (_ bv0 1))) (?v_17 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) R_EAX_5_89)) (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))) (?v_9 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134567760 32) (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134567760 32) (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134567760 32) (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134567760 32) (_ bv3 32)))) (_ bv24 32)))) (?v_10 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134567756 32) (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134567756 32) (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134567756 32) (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134567756 32) (_ bv3 32)))) (_ bv24 32))))) (let ((?v_11 (bvsub ?v_9 ?v_10))) (let ((?v_16 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_11 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))) (?v_12 (bvand (concat (_ bv0 31) (ite (bvult ?v_9 (_ bv1 32)) (_ bv1 1) (_ bv0 1))) (_ bv1 32)))) (let ((?v_14 (bvand ?v_12 (_ bv1 32)))) (let ((?v_13 (bvxor (bvxor (_ bv0 32) ?v_12) ?v_14))) (let ((?v_20 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_9 ?v_10) (bvxor ?v_9 ?v_11)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvor ?v_16 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_9 (_ bv1 32)) (bvxor ?v_9 (bvsub ?v_9 (_ bv1 32)))) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor (_ bv0 32) ?v_13) (bvxor (_ bv0 32) (bvsub (bvsub (_ bv0 32) ?v_13) ?v_14))) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand ?v_15 (_ bv1 1))))) (bvor (bvnot ?v_16) (_ bv1 1))))) (?v_23 (bvnot ?v_17)) (?v_18 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134534684 32) (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134534684 32) (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134534684 32) (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134534684 32) (_ bv3 32)))) (_ bv24 32))))) (let ((?v_19 (bvsub ?v_18 ?v_10))) (let ((?v_21 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_19 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))))) (= (_ bv1 1) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_0 (_ bv0 32)) (bvxor ?v_0 ?v_1)) (_ bv7 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvor ?v_24 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_3 (_ bv0 32)) (bvxor ?v_3 ?v_4)) (_ bv7 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvor ?v_22 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_6 (_ bv0 32)) (bvxor ?v_6 ?v_7)) (_ bv7 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvor ?v_8 (_ bv1 1)) (bvor (bvnot ?v_8) (bvand ?v_15 (bvand (bvor ?v_17 ?v_20) (bvor ?v_23 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_18 ?v_10) (bvxor ?v_18 ?v_19)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvor ?v_21 ?v_20) (bvor (bvnot ?v_21) (_ bv1 1))))))))))) (bvor (bvnot ?v_22) (bvand ?v_15 (bvand (bvor ?v_17 (_ bv1 1)) (bvor ?v_23 (_ bv1 1)))))))) (bvor (bvnot ?v_24) (_ bv1 1)))))))))))))))))))))
-(check-sat)
-(exit)

UnitTests/sat/QF_ABVFP/query.045.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_ABVFP)
-(set-info :source |
-Generated by: Daniel Liew, Daniel Schemmel, Cristian Cadar, Alastair Donaldson, and Rafael Zähl
-Generated on: 2017-4-28
-Generator: KLEE
-Application: Branch satisfiability check for symbolic execution of C programs
-Target solver: Z3 or MathSAT5
-Corresponding query: An equisatisfiable query (arrays replaced with bitvectors) is available at QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_memcpy_and_use_as_bitvector_klee.x86_64/query.045.smt2
-|)
-(set-info :license "https://creativecommons.org/licenses/by/4.0/")
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun fresh_to_ieee_bv_!0 () (_ BitVec 32))
-(declare-fun f0 () (Array (_ BitVec 32) (_ BitVec 8)))
-(assert
- (let ((?x15 (concat (select f0 (_ bv2 32)) (concat (select f0 (_ bv1 32)) (select f0 (_ bv0 32))))))
- (let ((?x23 (fp.add roundNearestTiesToEven ((_ to_fp 8 24) (concat (select f0 (_ bv3 32)) ?x15)) ((_ to_fp 8 24) (_ bv1065353216 32)))))
- (= ?x23 ((_ to_fp 8 24) fresh_to_ieee_bv_!0)))))
-(assert
- (not (not (bvslt (_ bv0 32) (bvand fresh_to_ieee_bv_!0 (_ bv16 32))))))
-(check-sat)
-(exit)

UnitTests/sat/QF_BVFP/query.2.smt2

@@ -6,47 +6,19 @@ Generated on: 2017-4-28
 Generator: KLEE
 Application: Branch satisfiability check for symbolic execution of C programs
 Target solver: Z3 or MathSAT5
-Corresponding query: An equisatisfiable query (bitvectors replaced with reads from arrays of bitvectors) is available at QF_ABVFP/20170428-Liew-KLEE/aachen_syn_sqr_float-noflow.x86_64/query.2.smt2
+Corresponding query: An equisatisfiable query (bitvectors replaced with reads from arrays of bitvectors) is available at QF_ABVFP/20170428-Liew-KLEE/imperial_svcomp_float-benchs_svcomp_arctan_Pade.x86_64/query.2.smt2
 |)
 (set-info :license "https://creativecommons.org/licenses/by/4.0/")
 (set-info :category "industrial")
 (set-info :status sat)
-(declare-fun f_ackermann!0 () (_ BitVec 32))
+(declare-fun symbolic_0_double_ackermann!0 () (_ BitVec 64))
 (assert
- (not (fp.isNaN ((_ to_fp 8 24) f_ackermann!0))))
+ (let ((?x8 ((_ to_fp 11 53) symbolic_0_double_ackermann!0)))
+ (fp.geq ?x8 ((_ to_fp 11 53) (_ bv18442201928238480281 64)))))
 (assert
- (let ((?x13 ((_ to_fp 11 53) roundNearestTiesToEven (fp.abs ((_ to_fp 8 24) f_ackermann!0)))))
- (let ((?x16 (fp.mul roundNearestTiesToEven ?x13 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
- (not (fp.isNaN ?x16)))))
+ (let ((?x8 ((_ to_fp 11 53) symbolic_0_double_ackermann!0)))
+ (fp.leq ?x8 ((_ to_fp 11 53) (_ bv9218829891383704473 64)))))
 (assert
- (let ((?x8 ((_ to_fp 8 24) f_ackermann!0)))
- (let ((?x20 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
- (let ((?x21 ((_ to_fp 11 53) roundNearestTiesToEven ?x20)))
- (not (fp.isNaN ?x21))))))
-(assert
- (let ((?x8 ((_ to_fp 8 24) f_ackermann!0)))
- (let ((?x20 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
- (let ((?x21 ((_ to_fp 11 53) roundNearestTiesToEven ?x20)))
- (let ((?x13 ((_ to_fp 11 53) roundNearestTiesToEven (fp.abs ?x8))))
- (let ((?x16 (fp.mul roundNearestTiesToEven ?x13 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
- (not (fp.gt ?x16 ?x21))))))))
-(assert
- (let ((?x13 ((_ to_fp 11 53) roundNearestTiesToEven (fp.abs ((_ to_fp 8 24) f_ackermann!0)))))
- (not (fp.isNaN ?x13))))
-(assert
- (let ((?x8 ((_ to_fp 8 24) f_ackermann!0)))
- (let ((?x20 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
- (let ((?x21 ((_ to_fp 11 53) roundNearestTiesToEven ?x20)))
- (let ((?x28 (fp.mul roundNearestTiesToEven ?x21 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
- (not (fp.isNaN ?x28)))))))
-(assert
- (let ((?x8 ((_ to_fp 8 24) f_ackermann!0)))
- (let ((?x20 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
- (let ((?x21 ((_ to_fp 11 53) roundNearestTiesToEven ?x20)))
- (let ((?x28 (fp.mul roundNearestTiesToEven ?x21 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
- (let ((?x13 ((_ to_fp 11 53) roundNearestTiesToEven (fp.abs ?x8))))
- (not (fp.lt ?x13 ?x28))))))))
-(assert
- (not false))
+ (not (not (fp.lt ((_ to_fp 11 53) symbolic_0_double_ackermann!0) ((_ to_fp 11 53) (_ bv0 64))))))
 (check-sat)
 (exit)

UnitTests/sat/QF_FP/assoc_mult.smt2

@@ -4,7 +4,6 @@
 (set-info :source |SPARK inspired floating point problems by Florian Schanda and Martin Brain|)
 (set-info :category "crafted")
 (set-info :status sat)
-(set-option :produce-models true)
 (define-fun is_finite ((f Float32)) Bool (or (fp.isZero f) (fp.isNormal f) (fp.isSubnormal f)))
 (declare-fun a () Float32)
 (declare-fun b () Float32)
@@ -18,5 +17,4 @@
 (assert (is_finite (fp.mul RNE (fp.mul RNE a b) c)))
 (assert (not (fp.eq (fp.mul RNE a (fp.mul RNE b c)) (fp.mul RNE (fp.mul RNE a b) c))))
 (check-sat)
-;(get-value (a b c))
 (exit)

UnitTests/sat/QF_FP/square_neg_id_fp_sat.smt2

@@ -17,6 +17,9 @@
 (define-fun two () Float64
   (fp #b0 #b10000000000 #b0000000000000000000000000000000000000000000000000000))
 
+(define-fun ndy () Float64
+  (fp.neg dy))
+
 (define-fun xmy2 () Float64
   (fp.mul RNE (fp.sub RNE dx dy) (fp.sub RNE dx dy)))
 
@@ -44,7 +47,8 @@
 	(isInsideAbsMax dy one)
 	(not (fp.isZero dy))
 	(isFinite diff))
-   (isInsideAbsMax diff max_diff))))
+   (= xmy2 id_xmy2))))
+;   (isInsideAbsMax diff max_diff))))
 
 (check-sat)
 

UnitTests/sat/QF_NIA/aproveSMT1357141816009857110.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun b__19 () Int)
-(declare-fun a__2 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__10 () Int)
-(declare-fun a__8 () Int)
-(declare-fun a__4 () Int)
-(declare-fun a__11 () Int)
-(declare-fun a__14 () Int)
-(declare-fun a__7 () Int)
-(declare-fun a__13 () Int)
-(declare-fun a__12 () Int)
-(declare-fun a__16 () Int)
-(declare-fun a__15 () Int)
-(declare-fun a__17 () Int)
-(declare-fun a__5 () Int)
-(declare-fun a__18 () Int)
-(declare-fun a__1 () Int)
-(declare-fun a__6 () Int)
-(declare-fun a__9 () Int)
-(assert (and (>= (+ 1 (* (- 0 1) b__19)) 0) (= (+ (* b__19 a__2) (* (- 0 1) a__2)) 0) (>= (+ a__3 (* (- 0 1) a__10)) 0) (>= (+ (* a__8 a__4) (* (- 0 1) a__11)) 0) (>= (+ a__10 (* (- 0 1) (* a__14 a__2)) (* (- 0 1) a__3)) 0) (>= (+ (* a__7 a__11) (* (- 0 1) (* a__13 a__2)) (* (- 0 1) (* a__7 a__4))) 0) (>= (+ (* a__8 a__11) (* (- 0 1) (* a__8 a__4))) 0) (>= (+ (* b__19 a__12) (* b__19 a__16 a__14) (* (- 0 1) (* b__19 a__15))) 0) (>= (+ (* b__19 a__12) (* b__19 a__16 a__13) (* b__19 a__17 a__14) (* (- 0 1) (* b__19 a__5))) 0) (>= (+ (* b__19 a__18 a__13) (* (- 0 1) (* b__19 a__13))) 0) (>= (+ (* b__19 a__18 a__14) (* (- 0 1) (* b__19 a__14))) 0) (>= (+ a__1 (* a__5 a__2) (* a__6 a__4) (* (- 0 1) a__9)) 0) (>= (+ a__9 (* a__6 a__11) (* (- 0 1) a__1) (* (- 0 1) (* a__12 a__2)) (* (- 0 1) (* a__6 a__4))) 0) (>= (+ a__1 (* a__15 a__2) (* a__6 a__4) (* (- 0 1) a__9)) 0) (not (and (= (+ a__1 (* a__5 a__2) (* a__6 a__4) (* (- 0 1) a__9)) 0) (= (+ a__9 (* a__6 a__11) (* (- 0 1) a__1) (* (- 0 1) (* a__12 a__2)) (* (- 0 1) (* a__6 a__4))) 0) (= (+ a__1 (* a__15 a__2) (* a__6 a__4) (* (- 0 1) a__9)) 0))) (>= b__19 0) (>= 1 b__19) (>= a__2 0) (>= a__3 0) (>= a__10 0) (>= a__8 0) (>= a__4 0) (>= a__11 0) (>= a__14 0) (>= a__7 0) (>= a__13 0) (>= a__12 0) (>= a__16 0) (>= a__15 0) (>= a__17 0) (>= a__5 0) (>= a__18 0) (>= a__1 0) (>= a__6 0) (>= a__9 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT1652619482144589486.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun b__9 () Int)
-(declare-fun a__2 () Int)
-(declare-fun a__6 () Int)
-(declare-fun a__4 () Int)
-(declare-fun a__8 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__5 () Int)
-(declare-fun a__7 () Int)
-(assert (and (>= (+ 1 (* (- 0 1) b__9)) 0) (= (+ (* b__9 a__2) (* (- 0 1) a__2)) 0) (>= (+ (* a__6 a__6 a__4 a__2) (* (- 0 1) (* a__4 a__2))) 0) (>= (+ (* a__6 a__6 a__4 a__2) (* (- 0 1) (* a__4 a__4 a__2))) 0) (>= (+ (* a__6 a__6 a__4 a__2) (* (- 0 1) a__2)) 0) (>= (+ (* a__8 a__2) (* (- 0 1) a__2)) 0) (>= (+ (* b__9 a__3) (* b__9 a__3 a__4) (* b__9 a__5 a__4 a__4) (* b__9 a__5 a__6 a__4 a__4) (* (- 0 1) (* b__9 a__5)) (* (- 0 1) (* b__9 a__5 a__6)) (* (- 0 1) (* b__9 a__5 a__6 a__6)) (* (- 0 1) (* b__9 a__3 a__6 a__6 a__6)) (* (- 0 1) (* b__9 a__3 a__4 a__6 a__6 a__6)) (* (- 0 1) (* b__9 a__3 a__4 a__4 a__6 a__6 a__6))) 0) (>= (+ (* b__9 a__6 a__6 a__4 a__4) (* (- 0 1) (* b__9 a__4 a__4 a__4 a__6 a__6 a__6))) 0) (>= (+ (* b__9 a__3) (* b__9 a__7 a__4) (* (- 0 1) (* b__9 a__7)) (* (- 0 1) (* b__9 a__3 a__8))) 0) (>= (+ (* b__9 a__7) (* b__9 a__5 a__8) (* (- 0 1) (* b__9 a__5)) (* (- 0 1) (* b__9 a__7 a__6))) 0) (>= (* a__5 a__4 a__2) 0) (>= (* a__5 a__6 a__4 a__2) 0) (>= (+ (* a__5 a__4 a__2) (* a__5 a__6 a__4 a__2) (* (- 0 1) (* a__3 a__4 a__2))) 0) (>= (* a__3 a__2) 0) (>= (* a__7 a__2) 0) (not (and (= (* a__5 a__4 a__2) 0) (= (* a__5 a__6 a__4 a__2) 0) (= (+ (* a__5 a__4 a__2) (* a__5 a__6 a__4 a__2) (* (- 0 1) (* a__3 a__4 a__2))) 0) (= (* a__3 a__2) 0) (= (* a__7 a__2) 0))) (>= b__9 0) (>= 1 b__9) (>= a__2 0) (>= a__6 0) (>= a__4 0) (>= a__8 0) (>= a__3 0) (>= a__5 0) (>= a__7 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT1673548157733187442.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun b__22 () Int)
-(declare-fun a__7 () Int)
-(declare-fun b__23 () Int)
-(declare-fun a__16 () Int)
-(declare-fun a__21 () Int)
-(declare-fun a__5 () Int)
-(declare-fun a__2 () Int)
-(declare-fun a__10 () Int)
-(declare-fun a__8 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__11 () Int)
-(declare-fun a__13 () Int)
-(declare-fun a__9 () Int)
-(declare-fun a__4 () Int)
-(declare-fun a__14 () Int)
-(declare-fun a__15 () Int)
-(declare-fun a__17 () Int)
-(declare-fun a__18 () Int)
-(declare-fun a__19 () Int)
-(declare-fun a__12 () Int)
-(declare-fun a__20 () Int)
-(declare-fun a__1 () Int)
-(declare-fun a__6 () Int)
-(assert (and (>= (+ 1 (* (- 0 1) b__22)) 0) (= (+ (* b__22 a__7) (* (- 0 1) a__7)) 0) (>= (+ 1 (* (- 0 1) b__23)) 0) (= (+ (* b__23 a__7 a__16) (* (- 0 1) (* a__7 a__16))) 0) (= (+ (* b__23 a__7 a__21) (* (- 0 1) (* a__7 a__21))) 0) (>= (+ (* a__5 a__2) (* (- 0 1) (* a__5 a__10 a__7)) (* (- 0 1) a__8)) 0) (>= (+ (* a__5 a__3) (* (- 0 1) (* a__11 a__7))) 0) (>= (+ (* a__13 a__7) (* (- 0 1) a__3)) 0) (>= (+ a__8 (* (- 0 1) a__2)) 0) (>= (+ (* a__5 a__2) (* (- 0 1) a__2)) 0) (>= (+ (* a__5 a__3) (* (- 0 1) a__3)) 0) (>= (+ (* b__22 a__9) (* b__22 a__4 a__10) (* b__22 a__14 a__11) (* (- 0 1) (* b__22 a__15)) (* (- 0 1) (* b__22 a__9 a__16)) (* (- 0 1) (* b__22 a__4 a__11 a__16)) (* (- 0 1) (* b__22 a__14 a__5 a__11 a__16))) 0) (>= (+ (* b__22 a__5 a__10) (* (- 0 1) (* b__22 a__10 a__16))) 0) (>= (+ (* b__22 a__9) (* b__22 a__4 a__10) (* b__22 a__4 a__11) (* (- 0 1) (* b__22 a__17)) (* (- 0 1) (* b__22 a__9 a__18)) (* (- 0 1) (* b__22 a__4 a__10 a__18))) 0) (>= (+ (* b__22 a__5 a__10) (* (- 0 1) (* b__22 a__5 a__10 a__18)) (* (- 0 1) (* b__22 a__19))) 0) (>= (+ (* b__22 a__5 a__11) (* (- 0 1) (* b__22 a__11 a__18))) 0) (>= (+ (* b__22 a__17) (* b__22 a__12 a__18) (* (- 0 1) (* b__22 a__20)) (* (- 0 1) (* b__22 a__9 a__21))) 0) (>= (+ (* b__22 a__13 a__18) (* (- 0 1) (* b__22 a__11 a__21))) 0) (>= (+ (* b__22 a__19) (* (- 0 1) (* b__22 a__10 a__21))) 0) (>= (+ (* b__23 a__9) (* b__23 a__14 a__10) (* (- 0 1) (* b__23 a__12)) (* (- 0 1) (* b__23 a__4 a__13))) 0) (>= (+ (* b__23 a__11) (* (- 0 1) (* b__23 a__5 a__13))) 0) (>= (+ (* b__22 a__15) (* b__22 a__12 a__16) (* (- 0 1) (* b__22 a__12))) 0) (>= (+ (* b__22 a__13 a__16) (* (- 0 1) (* b__22 a__13))) 0) (>= (+ (* b__22 a__20) (* b__22 a__12 a__21) (* (- 0 1) (* b__22 a__12))) 0) (>= (+ (* b__22 a__13 a__21) (* (- 0 1) (* b__22 a__13))) 0) (>= (+ a__1 (* a__4 a__2) (* a__4 a__3) (* (- 0 1) a__6) (* (- 0 1) (* a__9 a__7)) (* (- 0 1) (* a__4 a__10 a__7))) 0) (>= (+ a__6 (* a__12 a__7) (* (- 0 1) a__1)) 0) (>= (+ (* a__4 a__2) (* a__14 a__3) (* (- 0 1) (* a__4 a__3)) (* (- 0 1) (* a__14 a__5 a__3))) 0) (>= (* a__4 a__3) 0) (not (and (= (+ a__1 (* a__4 a__2) (* a__4 a__3) (* (- 0 1) a__6) (* (- 0 1) (* a__9 a__7)) (* (- 0 1) (* a__4 a__10 a__7))) 0) (= (+ a__6 (* a__12 a__7) (* (- 0 1) a__1)) 0) (= (+ (* a__4 a__2) (* a__14 a__3) (* (- 0 1) (* a__4 a__3)) (* (- 0 1) (* a__14 a__5 a__3))) 0) (= (* a__4 a__3) 0))) (>= b__22 0) (>= 1 b__22) (>= a__7 0) (>= b__23 0) (>= 1 b__23) (>= a__16 0) (>= a__21 0) (>= a__5 0) (>= a__2 0) (>= a__10 0) (>= a__8 0) (>= a__3 0) (>= a__11 0) (>= a__13 0) (>= a__9 0) (>= a__4 0) (>= a__14 0) (>= a__15 0) (>= a__17 0) (>= a__18 0) (>= a__19 0) (>= a__12 0) (>= a__20 0) (>= a__1 0) (>= a__6 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT1740983214503071791.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun b__17 () Int)
-(declare-fun a__7 () Int)
-(declare-fun a__4 () Int)
-(declare-fun a__2 () Int)
-(declare-fun a__10 () Int)
-(declare-fun a__8 () Int)
-(declare-fun a__5 () Int)
-(declare-fun a__11 () Int)
-(declare-fun a__9 () Int)
-(declare-fun a__14 () Int)
-(declare-fun a__12 () Int)
-(declare-fun a__15 () Int)
-(declare-fun a__13 () Int)
-(declare-fun a__16 () Int)
-(declare-fun a__1 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__6 () Int)
-(assert (and (>= (+ 1 (* (- 0 1) b__17)) 0) (= (+ (* b__17 a__7) (* (- 0 1) a__7)) 0) (>= (+ (* a__4 a__2) (* (- 0 1) (* a__10 a__7)) (* (- 0 1) (* a__4 a__8))) 0) (>= (+ (* a__4 a__5 a__2) (* (- 0 1) (* a__11 a__7)) (* (- 0 1) (* a__4 a__5 a__8))) 0) (>= (+ (* a__5 a__5 a__2) (* (- 0 1) (* a__5 a__5 a__8))) 0) (>= (+ (* a__4 a__8) (* (- 0 1) (* a__4 a__2))) 0) (>= (+ (* a__5 a__5 a__8) (* (- 0 1) (* a__5 a__2))) 0) (>= (+ (* a__4 a__5 a__8) (* (- 0 1) (* a__4 a__2))) 0) (>= (+ (* b__17 a__9) (* b__17 a__14 a__10) (* (- 0 1) (* b__17 a__12))) 0) (>= (+ (* b__17 a__9) (* b__17 a__15 a__10) (* b__17 a__14 a__11) (* (- 0 1) (* b__17 a__13))) 0) (>= (+ (* b__17 a__16 a__10) (* (- 0 1) (* b__17 a__10))) 0) (>= (+ (* b__17 a__16 a__11) (* (- 0 1) (* b__17 a__11))) 0) (>= (+ a__1 (* a__3 a__2) (* a__3 a__5 a__2) (* (- 0 1) a__6) (* (- 0 1) (* a__9 a__7)) (* (- 0 1) (* a__3 a__8)) (* (- 0 1) (* a__3 a__5 a__8))) 0) (>= (+ a__6 (* a__12 a__7) (* a__3 a__8) (* a__3 a__5 a__8) (* (- 0 1) a__1) (* (- 0 1) (* a__3 a__2))) 0) (>= (+ a__6 (* a__13 a__7) (* a__3 a__8) (* a__3 a__5 a__8) (* (- 0 1) a__1) (* (- 0 1) (* a__3 a__2))) 0) (not (and (= (+ a__1 (* a__3 a__2) (* a__3 a__5 a__2) (* (- 0 1) a__6) (* (- 0 1) (* a__9 a__7)) (* (- 0 1) (* a__3 a__8)) (* (- 0 1) (* a__3 a__5 a__8))) 0) (= (+ a__6 (* a__12 a__7) (* a__3 a__8) (* a__3 a__5 a__8) (* (- 0 1) a__1) (* (- 0 1) (* a__3 a__2))) 0) (= (+ a__6 (* a__13 a__7) (* a__3 a__8) (* a__3 a__5 a__8) (* (- 0 1) a__1) (* (- 0 1) (* a__3 a__2))) 0))) (>= b__17 0) (>= 1 b__17) (>= a__7 0) (>= a__4 0) (>= a__2 0) (>= a__10 0) (>= a__8 0) (>= a__5 0) (>= a__11 0) (>= a__9 0) (>= a__14 0) (>= a__12 0) (>= a__15 0) (>= a__13 0) (>= a__16 0) (>= a__1 0) (>= a__3 0) (>= a__6 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT1921934893170238498.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun a__5 () Int)
-(declare-fun a__2 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__4 () Int)
-(assert (and (>= (+ (* a__5 a__2) (* (- 0 1) a__2)) 0) (>= (+ a__3 (* (- 0 1) (* a__5 a__3))) 0) (>= (+ a__2 (* (- 0 1) (* a__5 a__2))) 0) (>= (+ (* a__5 a__5 a__5 a__3) (* (- 0 1) a__3)) 0) (>= (+ (* a__4 a__2) (* (- 0 1) (* a__4 a__3))) 0) (>= (+ (* a__4 a__3) (* a__4 a__5 a__3) (* a__4 a__5 a__5 a__3) (* (- 0 1) (* a__4 a__2))) 0) (not (and (= (+ (* a__4 a__2) (* (- 0 1) (* a__4 a__3))) 0) (= (+ (* a__4 a__3) (* a__4 a__5 a__3) (* a__4 a__5 a__5 a__3) (* (- 0 1) (* a__4 a__2))) 0))) (>= a__5 0) (>= a__2 0) (>= a__3 0) (>= a__4 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT2169947826556866694.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun b__20 () Int)
-(declare-fun a__2 () Int)
-(declare-fun a__4 () Int)
-(declare-fun a__6 () Int)
-(declare-fun a__8 () Int)
-(declare-fun a__10 () Int)
-(declare-fun a__5 () Int)
-(declare-fun a__11 () Int)
-(declare-fun a__13 () Int)
-(declare-fun a__12 () Int)
-(declare-fun a__15 () Int)
-(declare-fun a__7 () Int)
-(declare-fun a__14 () Int)
-(declare-fun a__16 () Int)
-(declare-fun a__18 () Int)
-(declare-fun a__17 () Int)
-(declare-fun a__19 () Int)
-(declare-fun a__9 () Int)
-(declare-fun a__3 () Int)
-(assert (and (>= (+ 1 (* (- 0 1) b__20)) 0) (= (+ (* b__20 a__2) (* (- 0 1) a__2)) 0) (>= (+ (* a__4 a__2) (* (- 0 1) (* a__6 a__2))) 0) (>= (+ (* a__8 a__2) (* (- 0 1) (* a__10 a__2))) 0) (>= (+ (* b__20 a__5) (* b__20 a__11 a__6) (* b__20 a__13 a__12 a__6) (* b__20 a__13 a__15 a__12 a__6) (* (- 0 1) (* b__20 a__7))) 0) (>= (+ (* b__20 a__14 a__15 a__12 a__6) (* (- 0 1) (* b__20 a__8))) 0) (>= (+ (* b__20 a__5) (* b__20 a__16 a__6) (* (- 0 1) (* b__20 a__7)) (* (- 0 1) (* b__20 a__13 a__8)) (* (- 0 1) (* b__20 a__16 a__15 a__8)) (* (- 0 1) (* b__20 a__18 a__17 a__15 a__8))) 0) (>= (+ (* b__20 a__17 a__6) (* (- 0 1) (* b__20 a__14 a__8)) (* (- 0 1) (* b__20 a__19 a__17 a__15 a__8))) 0) (>= (+ (* b__20 a__5) (* b__20 a__11 a__6) (* (- 0 1) (* b__20 a__11)) (* (- 0 1) (* b__20 a__5 a__12))) 0) (>= (+ (* b__20 a__5) (* b__20 a__13 a__6) (* (- 0 1) (* b__20 a__13)) (* (- 0 1) (* b__20 a__5 a__14))) 0) (>= (+ (* b__20 a__15 a__6) (* (- 0 1) (* b__20 a__15))) 0) (>= (+ (* b__20 a__5) (* b__20 a__16 a__6) (* (- 0 1) (* b__20 a__16)) (* (- 0 1) (* b__20 a__5 a__17))) 0) (>= (+ (* b__20 a__5) (* b__20 a__18 a__6) (* (- 0 1) (* b__20 a__18)) (* (- 0 1) (* b__20 a__5 a__19))) 0) (>= (+ (* b__20 a__9) (* b__20 a__11 a__10) (* (- 0 1) (* b__20 a__11)) (* (- 0 1) (* b__20 a__9 a__12))) 0) (>= (+ (* b__20 a__9) (* b__20 a__13 a__10) (* (- 0 1) (* b__20 a__13)) (* (- 0 1) (* b__20 a__9 a__14)) (* (- 0 1) (* b__20 a__9 a__15))) 0) (>= (+ (* b__20 a__9) (* b__20 a__16 a__10) (* (- 0 1) (* b__20 a__16)) (* (- 0 1) (* b__20 a__9 a__17))) 0) (>= (+ (* b__20 a__9) (* b__20 a__18 a__10) (* (- 0 1) (* b__20 a__18)) (* (- 0 1) (* b__20 a__9 a__19))) 0) (>= (+ (* b__20 a__13) (* b__20 a__7 a__14) (* (- 0 1) (* b__20 a__7)) (* (- 0 1) (* b__20 a__13 a__8))) 0) (>= (+ (* b__20 a__15) (* (- 0 1) (* b__20 a__15 a__8))) 0) (>= (+ (* b__20 a__13) (* b__20 a__3 a__14) (* b__20 a__3 a__15) (* (- 0 1) (* b__20 a__3)) (* (- 0 1) (* b__20 a__13 a__4))) 0) (>= (+ (* b__20 a__11) (* b__20 a__7 a__12) (* (- 0 1) (* b__20 a__7)) (* (- 0 1) (* b__20 a__11 a__8))) 0) (>= (+ (* b__20 a__11) (* b__20 a__3 a__12) (* (- 0 1) (* b__20 a__3)) (* (- 0 1) (* b__20 a__11 a__4))) 0) (>= (+ (* b__20 a__16) (* b__20 a__7 a__17) (* (- 0 1) (* b__20 a__7)) (* (- 0 1) (* b__20 a__16 a__8))) 0) (>= (+ (* b__20 a__16) (* b__20 a__3 a__17) (* (- 0 1) (* b__20 a__3)) (* (- 0 1) (* b__20 a__16 a__4))) 0) (>= (+ (* b__20 a__18) (* b__20 a__7 a__19) (* (- 0 1) (* b__20 a__7)) (* (- 0 1) (* b__20 a__18 a__8))) 0) (>= (+ (* b__20 a__18) (* b__20 a__3 a__19) (* (- 0 1) (* b__20 a__3)) (* (- 0 1) (* b__20 a__18 a__4))) 0) (>= (+ (* a__3 a__2) (* (- 0 1) (* a__5 a__2))) 0) (>= (+ (* a__7 a__2) (* (- 0 1) (* a__9 a__2))) 0) (not (and (= (+ (* a__3 a__2) (* (- 0 1) (* a__5 a__2))) 0) (= (+ (* a__7 a__2) (* (- 0 1) (* a__9 a__2))) 0))) (>= b__20 0) (>= 1 b__20) (>= a__2 0) (>= a__4 0) (>= a__6 0) (>= a__8 0) (>= a__10 0) (>= a__5 0) (>= a__11 0) (>= a__13 0) (>= a__12 0) (>= a__15 0) (>= a__7 0) (>= a__14 0) (>= a__16 0) (>= a__18 0) (>= a__17 0) (>= a__19 0) (>= a__9 0) (>= a__3 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT2322179511678559502.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun b__21 () Int)
-(declare-fun a__9 () Int)
-(declare-fun a__2 () Int)
-(declare-fun a__14 () Int)
-(declare-fun a__10 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__11 () Int)
-(declare-fun a__6 () Int)
-(declare-fun a__4 () Int)
-(declare-fun a__15 () Int)
-(declare-fun a__12 () Int)
-(declare-fun a__7 () Int)
-(declare-fun a__13 () Int)
-(declare-fun a__17 () Int)
-(declare-fun a__18 () Int)
-(declare-fun a__19 () Int)
-(declare-fun a__16 () Int)
-(declare-fun a__20 () Int)
-(declare-fun a__1 () Int)
-(declare-fun a__5 () Int)
-(declare-fun a__8 () Int)
-(assert (and (>= (+ 1 (* (- 0 1) b__21)) 0) (= (+ (* b__21 a__9) (* (- 0 1) a__9)) 0) (>= (+ a__2 (* (- 0 1) (* a__14 a__9)) (* (- 0 1) a__10)) 0) (>= (+ a__3 (* (- 0 1) a__11)) 0) (>= (+ (* a__6 a__4) (* (- 0 1) (* a__15 a__9)) (* (- 0 1) (* a__6 a__12))) 0) (>= (+ (* a__7 a__4) (* (- 0 1) (* a__7 a__12))) 0) (>= (+ a__10 (* (- 0 1) a__2)) 0) (>= (+ a__11 (* (- 0 1) a__3)) 0) (>= (+ (* a__7 a__12) (* (- 0 1) a__4)) 0) (>= (+ (* b__21 a__13) (* b__21 a__17 a__14) (* b__21 a__17 a__15) (* (- 0 1) (* b__21 a__18))) 0) (>= (+ (* b__21 a__13) (* b__21 a__17 a__14) (* b__21 a__19 a__15) (* (- 0 1) (* b__21 a__16))) 0) (>= (+ (* b__21 a__13) (* b__21 a__19 a__14) (* b__21 a__17 a__15) (* (- 0 1) (* b__21 a__16))) 0) (>= (+ (* b__21 a__20 a__14) (* (- 0 1) (* b__21 a__14))) 0) (>= (+ (* b__21 a__20 a__15) (* (- 0 1) (* b__21 a__15))) 0) (>= (+ a__1 (* a__5 a__4) (* (- 0 1) a__8) (* (- 0 1) (* a__13 a__9)) (* (- 0 1) (* a__5 a__12))) 0) (>= (+ a__8 (* a__16 a__9) (* a__5 a__12) (* (- 0 1) a__1)) 0) (not (and (= (+ a__1 (* a__5 a__4) (* (- 0 1) a__8) (* (- 0 1) (* a__13 a__9)) (* (- 0 1) (* a__5 a__12))) 0) (= (+ a__8 (* a__16 a__9) (* a__5 a__12) (* (- 0 1) a__1)) 0))) (>= b__21 0) (>= 1 b__21) (>= a__9 0) (>= a__2 0) (>= a__14 0) (>= a__10 0) (>= a__3 0) (>= a__11 0) (>= a__6 0) (>= a__4 0) (>= a__15 0) (>= a__12 0) (>= a__7 0) (>= a__13 0) (>= a__17 0) (>= a__18 0) (>= a__19 0) (>= a__16 0) (>= a__20 0) (>= a__1 0) (>= a__5 0) (>= a__8 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT2432885399846559546.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun a__2 () Int)
-(declare-fun a__5 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__6 () Int)
-(declare-fun a__7 () Int)
-(declare-fun a__10 () Int)
-(declare-fun a__1 () Int)
-(declare-fun a__4 () Int)
-(declare-fun a__8 () Int)
-(declare-fun a__9 () Int)
-(assert (and (>= (+ a__2 (* (- 0 1) a__5)) 0) (>= (+ a__3 (* (- 0 1) a__6) (* (- 0 1) a__7)) 0) (>= (+ a__5 (* (- 0 1) a__2)) 0) (>= (+ (* a__10 a__7) (* (- 0 1) (* a__10 a__3))) 0) (>= (+ a__1 (* (- 0 1) a__4)) 0) (>= (+ a__4 (* a__8 a__6) (* a__9 a__7) (* (- 0 1) a__1) (* (- 0 1) (* a__9 a__3))) 0) (not (and (= (+ a__1 (* (- 0 1) a__4)) 0) (= (+ a__4 (* a__8 a__6) (* a__9 a__7) (* (- 0 1) a__1) (* (- 0 1) (* a__9 a__3))) 0))) (>= a__2 0) (>= a__5 0) (>= a__3 0) (>= a__6 0) (>= a__7 0) (>= a__10 0) (>= a__1 0) (>= a__4 0) (>= a__8 0) (>= a__9 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT2440441682081812101.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun b__23 () Int)
-(declare-fun a__8 () Int)
-(declare-fun a__9 () Int)
-(declare-fun a__5 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__11 () Int)
-(declare-fun a__13 () Int)
-(declare-fun a__15 () Int)
-(declare-fun a__4 () Int)
-(declare-fun a__16 () Int)
-(declare-fun a__10 () Int)
-(declare-fun a__17 () Int)
-(declare-fun a__19 () Int)
-(declare-fun a__20 () Int)
-(declare-fun a__18 () Int)
-(declare-fun a__21 () Int)
-(declare-fun a__12 () Int)
-(declare-fun a__22 () Int)
-(declare-fun a__14 () Int)
-(declare-fun a__1 () Int)
-(declare-fun a__6 () Int)
-(declare-fun a__2 () Int)
-(declare-fun a__7 () Int)
-(assert (and (>= (+ 1 (* (- 0 1) b__23)) 0) (= (+ (* b__23 a__8) (* (- 0 1) a__8)) 0) (= (+ (* b__23 a__9) (* (- 0 1) a__9)) 0) (= (+ (* b__23 a__5) (* (- 0 1) a__5)) 0) (>= (+ a__3 (* (- 0 1) (* a__11 a__8))) 0) (>= (+ a__5 (* (- 0 1) (* a__11 a__9))) 0) (>= (+ (* a__13 a__8) (* (- 0 1) a__3)) 0) (>= (+ (* a__15 a__9) (* (- 0 1) a__4)) 0) (>= (+ (* a__16 a__9) (* (- 0 1) (* a__11 a__5))) 0) (>= (+ (* b__23 a__10) (* b__23 a__17 a__11) (* (- 0 1) (* b__23 a__19)) (* (- 0 1) (* b__23 a__10 a__20))) 0) (>= (+ (* b__23 a__18 a__11) (* (- 0 1) (* b__23 a__11 a__20))) 0) (>= (+ (* b__23 a__10) (* b__23 a__21 a__11) (* (- 0 1) (* b__23 a__12)) (* (- 0 1) (* b__23 a__10 a__13))) 0) (>= (+ (* b__23 a__22 a__11) (* (- 0 1) (* b__23 a__11 a__13))) 0) (>= (+ (* b__23 a__11) (* (- 0 1) b__23)) 0) (>= (+ (* b__23 a__12) (* (- 0 1) (* b__23 a__21))) 0) (>= (+ (* b__23 a__13) (* (- 0 1) (* b__23 a__22))) 0) (>= (+ (* b__23 a__19) (* (- 0 1) (* b__23 a__14)) (* (- 0 1) (* b__23 a__17 a__16)) (* (- 0 1) (* b__23 a__21 a__18 a__16))) 0) (>= (+ (* b__23 a__20) (* (- 0 1) (* b__23 a__15)) (* (- 0 1) (* b__23 a__22 a__18 a__16))) 0) (>= (+ (* b__23 a__19) (* (- 0 1) (* b__23 a__17))) 0) (>= (+ (* b__23 a__20) (* (- 0 1) (* b__23 a__18))) 0) (>= (+ a__1 (* a__6 a__2) (* (- 0 1) a__7) (* (- 0 1) (* a__10 a__8)) (* (- 0 1) (* a__10 a__9))) 0) (>= (+ a__7 (* a__12 a__8) (* a__14 a__9) (* (- 0 1) a__1) (* (- 0 1) (* a__6 a__2)) (* (- 0 1) (* a__10 a__5))) 0) (not (and (= (+ a__1 (* a__6 a__2) (* (- 0 1) a__7) (* (- 0 1) (* a__10 a__8)) (* (- 0 1) (* a__10 a__9))) 0) (= (+ a__7 (* a__12 a__8) (* a__14 a__9) (* (- 0 1) a__1) (* (- 0 1) (* a__6 a__2)) (* (- 0 1) (* a__10 a__5))) 0))) (>= b__23 0) (>= 1 b__23) (>= a__8 0) (>= a__9 0) (>= a__5 0) (>= a__3 0) (>= a__11 0) (>= a__13 0) (>= a__15 0) (>= a__4 0) (>= a__16 0) (>= a__10 0) (>= a__17 0) (>= a__19 0) (>= a__20 0) (>= a__18 0) (>= a__21 0) (>= a__12 0) (>= a__22 0) (>= a__14 0) (>= a__1 0) (>= a__6 0) (>= a__2 0) (>= a__7 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT2924484866315781736.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun a__6 () Int)
-(declare-fun a__2 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__4 () Int)
-(declare-fun a__5 () Int)
-(assert (and (>= (+ (* a__6 a__2) (* (- 0 1) a__2)) 0) (>= (+ (* a__6 a__3) (* (- 0 1) a__3)) 0) (>= (+ (* a__4 a__2) (* (- 0 1) (* a__5 a__2)) (* (- 0 1) (* a__4 a__6 a__2))) 0) (>= (* a__5 a__2) 0) (>= (* a__5 a__3) 0) (not (and (= (+ (* a__4 a__2) (* (- 0 1) (* a__5 a__2)) (* (- 0 1) (* a__4 a__6 a__2))) 0) (= (* a__5 a__2) 0) (= (* a__5 a__3) 0))) (>= a__6 0) (>= a__2 0) (>= a__3 0) (>= a__4 0) (>= a__5 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT3045448966019955240.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun a__2 () Int)
-(declare-fun a__4 () Int)
-(declare-fun a__6 () Int)
-(declare-fun a__8 () Int)
-(declare-fun a__10 () Int)
-(declare-fun a__12 () Int)
-(declare-fun a__1 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__5 () Int)
-(declare-fun a__7 () Int)
-(declare-fun a__9 () Int)
-(declare-fun a__11 () Int)
-(assert (and (>= (+ a__2 (* (- 0 1) a__4)) 0) (>= (+ (* a__6 a__4) (* (- 0 1) a__8)) 0) (>= (+ (* a__10 a__8) (* (- 0 1) (* a__6 a__6 a__12 a__2))) 0) (>= (+ a__1 (* (- 0 1) a__3)) 0) (>= (+ a__3 (* a__5 a__4) (* (- 0 1) a__7)) 0) (>= (+ a__7 (* a__9 a__8) (* (- 0 1) a__1) (* (- 0 1) (* a__5 a__2)) (* (- 0 1) (* a__11 a__6 a__2)) (* (- 0 1) (* a__5 a__12 a__6 a__2))) 0) (not (and (= (+ a__1 (* (- 0 1) a__3)) 0) (= (+ a__3 (* a__5 a__4) (* (- 0 1) a__7)) 0) (= (+ a__7 (* a__9 a__8) (* (- 0 1) a__1) (* (- 0 1) (* a__5 a__2)) (* (- 0 1) (* a__11 a__6 a__2)) (* (- 0 1) (* a__5 a__12 a__6 a__2))) 0))) (>= a__2 0) (>= a__4 0) (>= a__6 0) (>= a__8 0) (>= a__10 0) (>= a__12 0) (>= a__1 0) (>= a__3 0) (>= a__5 0) (>= a__7 0) (>= a__9 0) (>= a__11 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT3283555306553104167.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun b__31 () Int)
-(declare-fun a__15 () Int)
-(declare-fun a__16 () Int)
-(declare-fun a__26 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__4 () Int)
-(declare-fun a__5 () Int)
-(declare-fun a__9 () Int)
-(declare-fun a__10 () Int)
-(declare-fun a__11 () Int)
-(declare-fun a__13 () Int)
-(declare-fun a__18 () Int)
-(declare-fun a__24 () Int)
-(declare-fun a__20 () Int)
-(declare-fun a__25 () Int)
-(declare-fun a__21 () Int)
-(declare-fun a__12 () Int)
-(declare-fun a__27 () Int)
-(declare-fun a__29 () Int)
-(declare-fun a__28 () Int)
-(declare-fun a__30 () Int)
-(declare-fun a__19 () Int)
-(declare-fun a__17 () Int)
-(declare-fun a__1 () Int)
-(declare-fun a__6 () Int)
-(declare-fun a__2 () Int)
-(declare-fun a__7 () Int)
-(declare-fun a__8 () Int)
-(declare-fun a__14 () Int)
-(declare-fun a__22 () Int)
-(declare-fun a__23 () Int)
-(assert (and (>= (+ 1 (* (- 0 1) b__31)) 0) (= (+ (* b__31 a__15) (* (- 0 1) a__15)) 0) (= (+ (* b__31 a__16) (* (- 0 1) a__16)) 0) (= (+ (* b__31 a__26) (* (- 0 1) a__26)) 0) (= (+ (* b__31 a__3) (* (- 0 1) a__3)) 0) (= (+ (* b__31 a__4) (* (- 0 1) a__4)) 0) (= (+ (* b__31 a__5) (* (- 0 1) a__5)) 0) (= (+ (* b__31 a__9) (* (- 0 1) a__9)) 0) (= (+ (* b__31 a__10) (* (- 0 1) a__10)) 0) (= (+ (* b__31 a__11) (* (- 0 1) a__11)) 0) (>= (+ a__3 (* (- 0 1) (* a__13 a__9))) 0) (>= (+ a__4 (* (- 0 1) (* a__13 a__10))) 0) (>= (+ a__5 (* (- 0 1) (* a__13 a__11))) 0) (>= (+ a__9 (* (- 0 1) (* a__13 a__15))) 0) (>= (+ a__11 (* (- 0 1) (* a__13 a__16))) 0) (>= (+ (* a__18 a__15) (* (- 0 1) a__24)) 0) (>= (+ (* a__20 a__16) (* (- 0 1) a__25)) 0) (>= (+ (* a__21 a__16) (* (- 0 1) (* a__13 a__26))) 0) (>= (+ a__24 (* (- 0 1) (* a__13 a__3))) 0) (>= (+ a__25 (* (- 0 1) (* a__13 a__4))) 0) (>= (+ a__26 (* (- 0 1) (* a__13 a__5))) 0) (>= (+ (* b__31 a__12) (* b__31 a__27 a__13) (* (- 0 1) (* b__31 a__29))) 0) (>= (+ (* b__31 a__28 a__13) (* (- 0 1) (* b__31 a__30))) 0) (>= (+ (* b__31 a__13) (* (- 0 1) b__31)) 0) (>= (+ (* b__31 a__29) (* (- 0 1) (* b__31 a__19)) (* (- 0 1) (* b__31 a__27 a__21)) (* (- 0 1) (* b__31 a__17 a__28 a__21))) 0) (>= (+ (* b__31 a__30) (* (- 0 1) (* b__31 a__20)) (* (- 0 1) (* b__31 a__18 a__28 a__21))) 0) (>= (+ (* b__31 a__29) (* (- 0 1) (* b__31 a__27))) 0) (>= (+ (* b__31 a__30) (* (- 0 1) (* b__31 a__28))) 0) (>= (+ a__1 (* a__6 a__2) (* (- 0 1) a__7) (* (- 0 1) (* a__6 a__8)) (* (- 0 1) (* a__12 a__9)) (* (- 0 1) (* a__12 a__10)) (* (- 0 1) (* a__12 a__11))) 0) (>= (+ a__7 (* a__6 a__8) (* (- 0 1) a__14) (* (- 0 1) (* a__12 a__15)) (* (- 0 1) (* a__12 a__16))) 0) (>= (+ a__14 (* a__17 a__15) (* a__19 a__16) (* (- 0 1) a__22) (* (- 0 1) (* a__6 a__23)) (* (- 0 1) (* a__12 a__26))) 0) (>= (+ a__22 (* a__6 a__23) (* (- 0 1) a__1) (* (- 0 1) (* a__6 a__2)) (* (- 0 1) (* a__12 a__3)) (* (- 0 1) (* a__12 a__4)) (* (- 0 1) (* a__12 a__5))) 0) (not (and (= (+ a__1 (* a__6 a__2) (* (- 0 1) a__7) (* (- 0 1) (* a__6 a__8)) (* (- 0 1) (* a__12 a__9)) (* (- 0 1) (* a__12 a__10)) (* (- 0 1) (* a__12 a__11))) 0) (= (+ a__7 (* a__6 a__8) (* (- 0 1) a__14) (* (- 0 1) (* a__12 a__15)) (* (- 0 1) (* a__12 a__16))) 0) (= (+ a__14 (* a__17 a__15) (* a__19 a__16) (* (- 0 1) a__22) (* (- 0 1) (* a__6 a__23)) (* (- 0 1) (* a__12 a__26))) 0) (= (+ a__22 (* a__6 a__23) (* (- 0 1) a__1) (* (- 0 1) (* a__6 a__2)) (* (- 0 1) (* a__12 a__3)) (* (- 0 1) (* a__12 a__4)) (* (- 0 1) (* a__12 a__5))) 0))) (>= b__31 0) (>= 1 b__31) (>= a__15 0) (>= a__16 0) (>= a__26 0) (>= a__3 0) (>= a__4 0) (>= a__5 0) (>= a__9 0) (>= a__10 0) (>= a__11 0) (>= a__13 0) (>= a__18 0) (>= a__24 0) (>= a__20 0) (>= a__25 0) (>= a__21 0) (>= a__12 0) (>= a__27 0) (>= a__29 0) (>= a__28 0) (>= a__30 0) (>= a__19 0) (>= a__17 0) (>= a__1 0) (>= a__6 0) (>= a__2 0) (>= a__7 0) (>= a__8 0) (>= a__14 0) (>= a__22 0) (>= a__23 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT3753640489284717738.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun a__4 () Int)
-(declare-fun a__2 () Int)
-(declare-fun a__7 () Int)
-(declare-fun a__5 () Int)
-(declare-fun a__8 () Int)
-(declare-fun a__11 () Int)
-(declare-fun a__14 () Int)
-(declare-fun a__12 () Int)
-(declare-fun a__15 () Int)
-(declare-fun a__19 () Int)
-(declare-fun a__22 () Int)
-(declare-fun a__24 () Int)
-(declare-fun a__17 () Int)
-(declare-fun a__20 () Int)
-(declare-fun a__1 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__6 () Int)
-(declare-fun a__9 () Int)
-(declare-fun a__10 () Int)
-(declare-fun a__13 () Int)
-(declare-fun a__16 () Int)
-(declare-fun a__18 () Int)
-(declare-fun a__21 () Int)
-(declare-fun a__23 () Int)
-(assert (and (>= (+ (* a__4 a__2) (* (- 0 1) a__7)) 0) (>= (+ (* a__5 a__2) (* (- 0 1) a__8)) 0) (>= (+ a__8 (* (- 0 1) a__2)) 0) (>= (+ (* a__11 a__2) (* (- 0 1) a__14)) 0) (>= (+ (* a__12 a__2) (* (- 0 1) a__15)) 0) (>= (+ (* a__19 a__15) (* (- 0 1) a__2)) 0) (>= (+ (* a__22 a__2) (* (- 0 1) a__24)) 0) (>= (+ a__24 (* (- 0 1) a__2)) 0) (>= (+ (* a__17 a__14) (* (- 0 1) a__2)) 0) (>= (+ (* a__20 a__15) (* (- 0 1) a__2)) 0) (>= (+ (* a__17 a__7) (* (- 0 1) a__2)) 0) (>= (+ a__1 (* a__3 a__2) (* (- 0 1) a__6)) 0) (>= (+ a__6 (* a__9 a__7) (* (- 0 1) a__1)) 0) (>= (+ a__1 (* a__10 a__2) (* (- 0 1) a__13)) 0) (>= (+ a__13 (* a__16 a__14) (* a__18 a__15) (* (- 0 1) a__1)) 0) (>= (+ a__1 (* a__21 a__2) (* (- 0 1) a__23)) 0) (>= (+ a__23 (* (- 0 1) a__1)) 0) (>= (+ a__6 (* a__16 a__7) (* (- 0 1) a__1)) 0) (not (and (= (+ a__1 (* a__3 a__2) (* (- 0 1) a__6)) 0) (= (+ a__6 (* a__9 a__7) (* (- 0 1) a__1)) 0) (= (+ a__1 (* a__10 a__2) (* (- 0 1) a__13)) 0) (= (+ a__13 (* a__16 a__14) (* a__18 a__15) (* (- 0 1) a__1)) 0) (= (+ a__1 (* a__21 a__2) (* (- 0 1) a__23)) 0) (= (+ a__23 (* (- 0 1) a__1)) 0) (= (+ a__6 (* a__16 a__7) (* (- 0 1) a__1)) 0))) (>= a__4 0) (>= a__2 0) (>= a__7 0) (>= a__5 0) (>= a__8 0) (>= a__11 0) (>= a__14 0) (>= a__12 0) (>= a__15 0) (>= a__19 0) (>= a__22 0) (>= a__24 0) (>= a__17 0) (>= a__20 0) (>= a__1 0) (>= a__3 0) (>= a__6 0) (>= a__9 0) (>= a__10 0) (>= a__13 0) (>= a__16 0) (>= a__18 0) (>= a__21 0) (>= a__23 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT4002199347190543845.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun b__31 () Int)
-(declare-fun a__11 () Int)
-(declare-fun b__32 () Int)
-(declare-fun a__22 () Int)
-(declare-fun a__6 () Int)
-(declare-fun a__2 () Int)
-(declare-fun a__5 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__8 () Int)
-(declare-fun a__16 () Int)
-(declare-fun a__12 () Int)
-(declare-fun a__9 () Int)
-(declare-fun a__13 () Int)
-(declare-fun a__17 () Int)
-(declare-fun a__14 () Int)
-(declare-fun a__15 () Int)
-(declare-fun a__20 () Int)
-(declare-fun a__19 () Int)
-(declare-fun a__7 () Int)
-(declare-fun a__21 () Int)
-(declare-fun a__25 () Int)
-(declare-fun a__26 () Int)
-(declare-fun a__23 () Int)
-(declare-fun a__27 () Int)
-(declare-fun a__24 () Int)
-(declare-fun a__28 () Int)
-(declare-fun a__18 () Int)
-(declare-fun a__29 () Int)
-(declare-fun a__30 () Int)
-(declare-fun a__4 () Int)
-(declare-fun a__1 () Int)
-(declare-fun a__10 () Int)
-(assert (and (>= (+ 1 (* (- 0 1) b__31)) 0) (= (+ (* b__31 a__11) (* (- 0 1) a__11)) 0) (>= (+ 1 (* (- 0 1) b__32)) 0) (= (+ (* b__32 a__11 a__22) (* (- 0 1) (* a__11 a__22))) 0) (>= (+ (* a__6 a__2) (* (- 0 1) a__2)) 0) (>= (+ (* a__5 a__2) (* (- 0 1) a__2)) 0) (>= (+ (* a__5 a__3) (* (- 0 1) a__3)) 0) (>= (+ (* a__6 a__3) (* (- 0 1) a__3)) 0) (>= (+ (* a__8 a__2) (* (- 0 1) (* a__16 a__11)) (* (- 0 1) a__12)) 0) (>= (+ (* a__9 a__2) (* (- 0 1) a__13)) 0) (>= (+ a__3 (* (- 0 1) (* a__17 a__11)) (* (- 0 1) a__14)) 0) (>= (+ a__13 (* (- 0 1) a__2)) 0) (>= (+ a__14 (* (- 0 1) a__3)) 0) (>= (+ a__2 (* (- 0 1) (* a__17 a__11)) (* (- 0 1) a__14)) 0) (>= (+ (* a__8 a__3) (* (- 0 1) (* a__16 a__11)) (* (- 0 1) a__12)) 0) (>= (+ (* a__9 a__3) (* (- 0 1) a__13)) 0) (>= (+ (* b__31 a__15) (* b__31 a__20 a__17) (* (- 0 1) (* b__31 a__19))) 0) (>= (+ (* b__31 a__15) (* b__31 a__7 a__17) (* (- 0 1) (* b__31 a__21)) (* (- 0 1) (* b__31 a__25 a__22))) 0) (>= (+ (* b__31 a__16) (* (- 0 1) (* b__31 a__26 a__22)) (* (- 0 1) (* b__31 a__23))) 0) (>= (+ (* b__31 a__8 a__17) (* (- 0 1) (* b__31 a__27 a__22))) 0) (>= (+ (* b__31 a__9 a__17) (* (- 0 1) (* b__31 a__24))) 0) (>= (+ (* b__31 a__21) (* b__31 a__19 a__22) (* (- 0 1) (* b__31 a__15))) 0) (>= (+ (* b__31 a__23) (* (- 0 1) (* b__31 a__16))) 0) (>= (+ (* b__31 a__24) (* (- 0 1) (* b__31 a__17))) 0) (>= (+ (* b__32 a__25) (* b__32 a__28 a__26) (* b__32 a__28 a__27) (* (- 0 1) (* b__32 a__18))) 0) (>= (+ (* b__32 a__25) (* b__32 a__28 a__26) (* b__32 a__29 a__27) (* (- 0 1) (* b__32 a__19))) 0) (>= (+ (* b__32 a__25) (* b__32 a__29 a__26) (* b__32 a__28 a__27) (* (- 0 1) (* b__32 a__19))) 0) (>= (+ (* b__32 a__30 a__26) (* (- 0 1) (* b__32 a__26))) 0) (>= (+ (* b__32 a__30 a__27) (* (- 0 1) (* b__32 a__27))) 0) (>= (+ (* b__31 a__21) (* b__31 a__18 a__22) (* (- 0 1) (* b__31 a__18))) 0) (>= (* a__4 a__2) 0) (>= (* a__4 a__3) 0) (>= (+ a__1 (* a__7 a__2) (* (- 0 1) a__10) (* (- 0 1) (* a__15 a__11))) 0) (>= (+ a__10 (* a__18 a__11) (* (- 0 1) a__1)) 0) (>= (+ a__1 (* a__7 a__3) (* (- 0 1) a__10) (* (- 0 1) (* a__15 a__11))) 0) (>= (+ a__10 (* a__19 a__11) (* (- 0 1) a__1)) 0) (not (and (= (* a__4 a__2) 0) (= (* a__4 a__3) 0) (= (+ a__1 (* a__7 a__2) (* (- 0 1) a__10) (* (- 0 1) (* a__15 a__11))) 0) (= (+ a__10 (* a__18 a__11) (* (- 0 1) a__1)) 0) (= (+ a__1 (* a__7 a__3) (* (- 0 1) a__10) (* (- 0 1) (* a__15 a__11))) 0) (= (+ a__10 (* a__19 a__11) (* (- 0 1) a__1)) 0))) (>= b__31 0) (>= 1 b__31) (>= a__11 0) (>= b__32 0) (>= 1 b__32) (>= a__22 0) (>= a__6 0) (>= a__2 0) (>= a__5 0) (>= a__3 0) (>= a__8 0) (>= a__16 0) (>= a__12 0) (>= a__9 0) (>= a__13 0) (>= a__17 0) (>= a__14 0) (>= a__15 0) (>= a__20 0) (>= a__19 0) (>= a__7 0) (>= a__21 0) (>= a__25 0) (>= a__26 0) (>= a__23 0) (>= a__27 0) (>= a__24 0) (>= a__28 0) (>= a__18 0) (>= a__29 0) (>= a__30 0) (>= a__4 0) (>= a__1 0) (>= a__10 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)

UnitTests/sat/QF_NIA/aproveSMT4550048332700395826.smt2

-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |AProve team, see http://aprove.informatik.rwth-aachen.de/, submitted for SMT-COMP 2014|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun b__29 () Int)
-(declare-fun a__8 () Int)
-(declare-fun a__14 () Int)
-(declare-fun b__30 () Int)
-(declare-fun a__2 () Int)
-(declare-fun a__13 () Int)
-(declare-fun a__9 () Int)
-(declare-fun a__5 () Int)
-(declare-fun a__3 () Int)
-(declare-fun a__16 () Int)
-(declare-fun a__10 () Int)
-(declare-fun a__6 () Int)
-(declare-fun a__11 () Int)
-(declare-fun a__15 () Int)
-(declare-fun a__18 () Int)
-(declare-fun a__19 () Int)
-(declare-fun a__4 () Int)
-(declare-fun a__20 () Int)
-(declare-fun a__21 () Int)
-(declare-fun a__22 () Int)
-(declare-fun a__12 () Int)
-(declare-fun a__23 () Int)
-(declare-fun a__24 () Int)
-(declare-fun a__17 () Int)
-(declare-fun a__25 () Int)
-(declare-fun a__26 () Int)
-(declare-fun a__27 () Int)
-(declare-fun a__28 () Int)
-(declare-fun a__1 () Int)
-(declare-fun a__7 () Int)
-(assert (and (>= (+ 1 (* (- 0 1) b__29)) 0) (= (+ (* b__29 a__8 a__14) (* (- 0 1) (* a__8 a__14))) 0) (>= (+ 1 (* (- 0 1) b__30)) 0) (= (+ (* b__30 a__8) (* (- 0 1) a__8)) 0) (>= (+ a__2 (* (- 0 1) (* a__13 a__8)) (* (- 0 1) a__9)) 0) (>= (+ (* a__5 a__3) (* (- 0 1) (* a__16 a__14 a__8)) (* (- 0 1) a__10)) 0) (>= (+ (* a__6 a__3) (* (- 0 1) a__11)) 0) (>= (+ a__9 (* (- 0 1) a__2)) 0) (>= (+ a__11 (* (- 0 1) a__3)) 0) (>= (+ (* b__29 a__15) (* b__29 a__18 a__16) (* (- 0 1) (* b__29 a__19))) 0) (>= (+ (* b__29 a__15) (* b__29 a__4 a__16) (* (- 0 1) (* b__29 a__20))) 0) (>= (+ (* b__29 a__5 a__16) (* (- 0 1) (* b__29 a__21))) 0) (>= (+ (* b__29 a__6 a__16) (* (- 0 1) (* b__29 a__22))) 0) (>= (+ (* b__30 a__12) (* b__30 a__19 a__13) (* b__30 a__19 a__14) (* (- 0 1) (* b__30 a__23))) 0) (>= (+ (* b__30 a__12) (* b__30 a__19 a__13) (* b__30 a__24 a__14) (* (- 0 1) (* b__30 a__17))) 0) (>= (+ (* b__30 a__12) (* b__30 a__24 a__13) (* b__30 a__19 a__14) (* (- 0 1) (* b__30 a__17))) 0) (>= (+ (* b__30 a__25 a__13) (* (- 0 1) (* b__30 a__13))) 0) (>= (+ (* b__30 a__25 a__14) (* (- 0 1) (* b__30 a__14))) 0) (>= (+ (* b__29 a__21) (* (- 0 1) b__29)) 0) (>= (+ (* b__29 a__4 a__22) (* b__29 a__26 a__5 a__22) (* (- 0 1) (* b__29 a__24 a__21)) (* (- 0 1) (* b__29 a__27 a__25 a__21))) 0) (>= (+ (* b__29 a__21) (* (- 0 1) (* b__29 a__28 a__25 a__21))) 0) (>= (+ (* b__29 a__6 a__22) (* (- 0 1) (* b__29 a__22))) 0) (>= (+ (* b__29 a__4 a__22) (* b__29 a__19 a__5 a__22) (* (- 0 1) (* b__29 a__27 a__21))) 0) (>= (+ (* b__29 a__21) (* (- 0 1) (* b__29 a__28 a__21))) 0) (>= (+ a__1 (* a__4 a__3) (* (- 0 1) a__7) (* (- 0 1) (* a__12 a__8)) (* (- 0 1) (* a__15 a__14 a__8))) 0) (>= (+ a__7 (* a__17 a__8) (* (- 0 1) a__1)) 0) (not (and (= (+ a__1 (* a__4 a__3) (* (- 0 1) a__7) (* (- 0 1) (* a__12 a__8)) (* (- 0 1) (* a__15 a__14 a__8))) 0) (= (+ a__7 (* a__17 a__8) (* (- 0 1) a__1)) 0))) (>= b__29 0) (>= 1 b__29) (>= a__8 0) (>= a__14 0) (>= b__30 0) (>= 1 b__30) (>= a__2 0) (>= a__13 0) (>= a__9 0) (>= a__5 0) (>= a__3 0) (>= a__16 0) (>= a__10 0) (>= a__6 0) (>= a__11 0) (>= a__15 0) (>= a__18 0) (>= a__19 0) (>= a__4 0) (>= a__20 0) (>= a__21 0) (>= a__22 0) (>= a__12 0) (>= a__23 0) (>= a__24 0) (>= a__17 0) (>= a__25 0) (>= a__26 0) (>= a__27 0) (>= a__28 0) (>= a__1 0) (>= a__7 0)))
-(check-sat)
-;;(get-assignment)
-;;(get-model)
-(exit)