Add few tests.

tests/data/ARI118=1.smt2

@@ -0,0 +1,16 @@
+(set-info :smt-lib-version 2.6)
+(set-logic BV)
+(set-info :source |These benchmarks are translations from the TPTP Library (Thousands of
+Problems for Theorem Provers), see http://www.cs.miami.edu/~tptp/
+
+The TPTP is maintained by Geoff Sutcliffe, and he contributed this
+selection of benchmarks to SMT-LIB.
+
+Translated to BV by Mathias Preiner.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+(assert (not (exists ((?X (_ BitVec 32)) (?Y (_ BitVec 32))) (= (bvmul ?X ?Y) ?X))))
+(check-sat)
+(exit)

tests/data/ETCS-essentials-node3023.smt2

@@ -0,0 +1,35 @@
+(set-info :smt-lib-version 2.6)
+(set-logic BV)
+(set-info :source |
+These benchmarks used in the paper:
+
+  Dejan Jovanovic and Leonardo de Moura.  Solving Non-Linear Arithmetic.
+  In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
+
+The keymaera family contains VCs from Keymaera verification, see:
+
+  A. Platzer, J.-D. Quesel, and P. Rummer.  Real world verification.
+  In CADE 2009, pages 485-501. Springer, 2009.
+
+Submitted by Dejan Jovanovic for SMT-LIB.
+
+ KeYmaera example: ETCS-essentials, node 3023 For more info see: @see "Andre Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2), pages 143-189, 2008."
+
+Translated to BV by Mathias Preiner.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+(declare-fun v () (_ BitVec 32))
+(declare-fun vuscore2dollarskuscore0 () (_ BitVec 32))
+(declare-fun b () (_ BitVec 32))
+(declare-fun A () (_ BitVec 32))
+(declare-fun t1uscore0dollarskuscore0 () (_ BitVec 32))
+(declare-fun ep () (_ BitVec 32))
+(declare-fun m () (_ BitVec 32))
+(declare-fun zuscore2dollarskuscore0 () (_ BitVec 32))
+(declare-fun ts1uscore0 () (_ BitVec 32))
+(declare-fun z () (_ BitVec 32))
+(assert (not (exists ((ts1uscore0 (_ BitVec 32))) (let ((?v_3 (bvneg b)) (?v_1 (bvmul (_ bv2 32) b)) (?v_0 (bvmul vuscore2dollarskuscore0 vuscore2dollarskuscore0)) (?v_2 (bvsub m zuscore2dollarskuscore0))) (let ((?v_4 (bvadd (bvmul ?v_3 t1uscore0dollarskuscore0) vuscore2dollarskuscore0))) (=> (and (and (and (and (and (and (=> (and (bvsle (_ bv0 32) ts1uscore0) (bvsle ts1uscore0 t1uscore0dollarskuscore0)) (and (bvsge (bvadd (bvmul ?v_3 ts1uscore0) vuscore2dollarskuscore0) (_ bv0 32)) (bvsle ts1uscore0 ep))) (bvsge t1uscore0dollarskuscore0 (_ bv0 32))) (bvsle ?v_2 (bvadd (bvsdiv ?v_0 ?v_1) (bvmul (bvadd (bvsdiv A b) (_ bv1 32)) (bvadd (bvmul (bvsdiv A (_ bv2 32)) (bvmul ep ep)) (bvmul ep vuscore2dollarskuscore0)))))) (bvsle ?v_0 (bvmul ?v_1 ?v_2))) (bvsle (bvmul v v) (bvmul ?v_1 (bvsub m z)))) (bvsgt b (_ bv0 32))) (bvsge A (_ bv0 32))) (bvsle (bvmul ?v_4 ?v_4) (bvmul ?v_1 (bvsub m (bvmul (bvsdiv (_ bv1 32) (_ bv2 32)) (bvadd (bvadd (bvmul ?v_3 (bvmul t1uscore0dollarskuscore0 t1uscore0dollarskuscore0)) (bvmul (bvmul (_ bv2 32) t1uscore0dollarskuscore0) vuscore2dollarskuscore0)) (bvmul (_ bv2 32) zuscore2dollarskuscore0))))))))))))
+(check-sat)
+(exit)

tests/data/accelerating-node2100.smt2

@@ -0,0 +1,35 @@
+(set-info :smt-lib-version 2.6)
+(set-logic BV)
+(set-info :source |
+These benchmarks used in the paper:
+
+  Dejan Jovanovic and Leonardo de Moura.  Solving Non-Linear Arithmetic.
+  In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
+
+The keymaera family contains VCs from Keymaera verification, see:
+
+  A. Platzer, J.-D. Quesel, and P. Rummer.  Real world verification.
+  In CADE 2009, pages 485-501. Springer, 2009.
+
+Submitted by Dejan Jovanovic for SMT-LIB.
+
+ KeYmaera example: accelerating, node 2100 For more info see: @see @see "Andre Platzer and Jan-David Quesel. European Train Control System: A case study in formal verification. In Karin Breitman and Ana Cavalcanti, editors, 11th International Conference on Formal Engineering Methods, ICFEM, Rio de Janeiro, Brasil, Proceedings, volume 5885 of LNCS, pages 246-265. Springer, 2009." 
+
+Translated to BV by Mathias Preiner.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+(declare-fun v () (_ BitVec 32))
+(declare-fun b () (_ BitVec 32))
+(declare-fun vuscore2dollarskuscore0 () (_ BitVec 32))
+(declare-fun A () (_ BitVec 32))
+(declare-fun ts2uscore0 () (_ BitVec 32))
+(declare-fun ep () (_ BitVec 32))
+(declare-fun m () (_ BitVec 32))
+(declare-fun zuscore2dollarskuscore0 () (_ BitVec 32))
+(declare-fun t2uscore0dollarskuscore0 () (_ BitVec 32))
+(declare-fun z () (_ BitVec 32))
+(assert (not (exists ((ts2uscore0 (_ BitVec 32))) (let ((?v_1 (bvmul (_ bv2 32) b)) (?v_0 (bvmul vuscore2dollarskuscore0 vuscore2dollarskuscore0)) (?v_2 (bvsub m zuscore2dollarskuscore0)) (?v_3 (bvadd (bvmul A t2uscore0dollarskuscore0) vuscore2dollarskuscore0))) (=> (and (and (and (and (and (and (=> (and (bvsle (_ bv0 32) ts2uscore0) (bvsle ts2uscore0 t2uscore0dollarskuscore0)) (and (bvsge (bvadd (bvmul A ts2uscore0) vuscore2dollarskuscore0) (_ bv0 32)) (bvsle ts2uscore0 ep))) (bvsge t2uscore0dollarskuscore0 (_ bv0 32))) (bvsge ?v_2 (bvadd (bvsdiv ?v_0 ?v_1) (bvmul (bvadd (bvsdiv A b) (_ bv1 32)) (bvadd (bvmul (bvsdiv A (_ bv2 32)) (bvmul ep ep)) (bvmul ep vuscore2dollarskuscore0)))))) (bvsle ?v_0 (bvmul ?v_1 ?v_2))) (bvsle (bvmul v v) (bvmul ?v_1 (bvsub m z)))) (bvsgt b (_ bv0 32))) (bvsge A (_ bv0 32))) (bvsle (bvmul ?v_3 ?v_3) (bvmul ?v_1 (bvsub m (bvmul (bvsdiv (_ bv1 32) (_ bv2 32)) (bvadd (bvadd (bvmul A (bvmul t2uscore0dollarskuscore0 t2uscore0dollarskuscore0)) (bvmul (bvmul (_ bv2 32) t2uscore0dollarskuscore0) vuscore2dollarskuscore0)) (bvmul (_ bv2 32) zuscore2dollarskuscore0)))))))))))
+(check-sat)
+(exit)

tests/data/binary_driver-2007-10-09-node11383.smt2

@@ -0,0 +1,40 @@
+(set-info :smt-lib-version 2.6)
+(set-logic BV)
+(set-info :source |
+These benchmarks used in the paper:
+
+  Dejan Jovanovic and Leonardo de Moura.  Solving Non-Linear Arithmetic.
+  In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
+
+The keymaera family contains VCs from Keymaera verification, see:
+
+  A. Platzer, J.-D. Quesel, and P. Rummer.  Real world verification.
+  In CADE 2009, pages 485-501. Springer, 2009.
+
+Submitted by Dejan Jovanovic for SMT-LIB.
+
+ KeYmaera example: binary_driver-2007-10-09, node 11383 For more info see: No further information available.
+
+Translated to BV by Mathias Preiner.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+(declare-fun ts4uscore0 () (_ BitVec 32))
+(declare-fun vuscore2dollarskuscore5 () (_ BitVec 32))
+(declare-fun duscore2dollarskuscore5 () (_ BitVec 32))
+(declare-fun d () (_ BitVec 32))
+(declare-fun b () (_ BitVec 32))
+(declare-fun vdesuscore2dollarskuscore4 () (_ BitVec 32))
+(declare-fun stateuscore2dollarskuscore2 () (_ BitVec 32))
+(declare-fun m () (_ BitVec 32))
+(declare-fun zuscore2dollarskuscore5 () (_ BitVec 32))
+(declare-fun v () (_ BitVec 32))
+(declare-fun ep () (_ BitVec 32))
+(declare-fun muscore2dollarskuscore5 () (_ BitVec 32))
+(declare-fun t4uscore0dollarskuscore0 () (_ BitVec 32))
+(declare-fun z () (_ BitVec 32))
+(declare-fun amax () (_ BitVec 32))
+(assert (not (exists ((ts4uscore0 (_ BitVec 32))) (let ((?v_1 (bvneg b)) (?v_0 (bvmul (_ bv2 32) b)) (?v_3 (bvmul duscore2dollarskuscore5 duscore2dollarskuscore5))) (let ((?v_2 (bvadd (bvmul ?v_1 t4uscore0dollarskuscore0) vuscore2dollarskuscore5))) (=> (and (and (and (and (and (and (and (and (and (and (and (and (=> (and (bvsle (_ bv0 32) ts4uscore0) (bvsle ts4uscore0 t4uscore0dollarskuscore0)) (and (bvsge (bvadd (bvmul ?v_1 ts4uscore0) vuscore2dollarskuscore5) (_ bv0 32)) (bvsle ts4uscore0 ep))) (bvsge t4uscore0dollarskuscore0 (_ bv0 32))) (= stateuscore2dollarskuscore2 (_ bv1 32))) (bvsge vuscore2dollarskuscore5 vdesuscore2dollarskuscore4)) (bvsle (bvsub (bvmul vuscore2dollarskuscore5 vuscore2dollarskuscore5) ?v_3) (bvmul ?v_0 (bvsub muscore2dollarskuscore5 zuscore2dollarskuscore5)))) (bvsge vuscore2dollarskuscore5 (_ bv0 32))) (bvsge duscore2dollarskuscore5 (_ bv0 32))) (bvsle (bvsub (bvmul v v) (bvmul d d)) (bvmul ?v_0 (bvsub m z)))) (bvsge v (_ bv0 32))) (bvsgt ep (_ bv0 32))) (bvsgt b (_ bv0 32))) (bvsgt amax (_ bv0 32))) (bvsge d (_ bv0 32))) (bvsle (bvsub (bvmul ?v_2 ?v_2) ?v_3) (bvmul ?v_0 (bvsub muscore2dollarskuscore5 (bvmul (bvsdiv (_ bv1 32) (_ bv2 32)) (bvadd (bvadd (bvmul ?v_1 (bvmul t4uscore0dollarskuscore0 t4uscore0dollarskuscore0)) (bvmul (bvmul (_ bv2 32) t4uscore0dollarskuscore0) vuscore2dollarskuscore5)) (bvmul (_ bv2 32) zuscore2dollarskuscore5))))))))))))
+(check-sat)
+(exit)

tests/data/magnetic_field-node118398.smt2

@@ -0,0 +1,39 @@
+(set-info :smt-lib-version 2.6)
+(set-logic BV)
+(set-info :source |
+These benchmarks used in the paper:
+
+  Dejan Jovanovic and Leonardo de Moura.  Solving Non-Linear Arithmetic.
+  In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
+
+The keymaera family contains VCs from Keymaera verification, see:
+
+  A. Platzer, J.-D. Quesel, and P. Rummer.  Real world verification.
+  In CADE 2009, pages 485-501. Springer, 2009.
+
+Submitted by Dejan Jovanovic for SMT-LIB.
+
+ KeYmaera example: magnetic_field, node 118398 For more info see: @see "Sriram Sankaranarayanan, Henny B. Sima, Zohar Manna: Constructing invariants for hybrid systems"
+
+Translated to BV by Mathias Preiner.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+(declare-fun stateuscore2dollarskuscore35 () (_ BitVec 32))
+(declare-fun b () (_ BitVec 32))
+(declare-fun ts17uscore0 () (_ BitVec 32))
+(declare-fun a () (_ BitVec 32))
+(declare-fun vyuscore2dollarskuscore27 () (_ BitVec 32))
+(declare-fun t17uscore0dollarskuscore0 () (_ BitVec 32))
+(declare-fun vy () (_ BitVec 32))
+(declare-fun vx () (_ BitVec 32))
+(declare-fun yuscore2dollarskuscore21 () (_ BitVec 32))
+(declare-fun xuscore2dollarskuscore22 () (_ BitVec 32))
+(declare-fun vxuscore2dollarskuscore26 () (_ BitVec 32))
+(declare-fun buscore2dollarskuscore35 () (_ BitVec 32))
+(declare-fun y () (_ BitVec 32))
+(declare-fun x () (_ BitVec 32))
+(assert (not (exists ((ts17uscore0 (_ BitVec 32))) (let ((?v_0 (bvadd vyuscore2dollarskuscore27 (_ bv2 32)))) (=> (and (and (and (and (and (and (and (and (and (and (and (= ?v_0 (bvmul a (bvsub (bvadd (bvmul t17uscore0dollarskuscore0 vxuscore2dollarskuscore26) xuscore2dollarskuscore22) (_ bv2 32)))) (= (bvadd (bvmul vxuscore2dollarskuscore26 vxuscore2dollarskuscore26) (bvmul vyuscore2dollarskuscore27 vyuscore2dollarskuscore27)) (_ bv8 32))) (= (bvsub vxuscore2dollarskuscore26 (_ bv2 32)) (bvadd (bvmul (bvneg a) (bvadd (bvadd (bvmul t17uscore0dollarskuscore0 vyuscore2dollarskuscore27) yuscore2dollarskuscore21) (_ bv2 32))) (bvmul (bvmul (_ bv4 32) buscore2dollarskuscore35) (bvsub (_ bv1 32) a))))) (= stateuscore2dollarskuscore35 (_ bv1 32))) (=> (and (bvsle (_ bv0 32) ts17uscore0) (bvsle ts17uscore0 t17uscore0dollarskuscore0)) (bvsle vxuscore2dollarskuscore26 (_ bv0 32)))) (bvsge t17uscore0dollarskuscore0 (_ bv0 32))) (= stateuscore2dollarskuscore35 (_ bv2 32))) (= vx (_ bv2 32))) (= vy (bvneg (_ bv2 32)))) (= x (_ bv0 32))) (= y (_ bv0 32))) (= b (_ bv0 32))) (or (or (= stateuscore2dollarskuscore35 (_ bv0 32)) (= ?v_0 (bvmul a (bvsub xuscore2dollarskuscore22 (_ bv2 32))))) (= ?v_0 (_ bv0 32))))))))
+(check-sat)
+(exit)

tests/main.cpp

@@ -74,13 +74,18 @@ TEST_CASE( "Without approximations", "[noapprox]" )
     REQUIRE( SolveWithoutApprox("../tests/data/falseAndFalse.smt2") == UNSAT );
     REQUIRE( SolveWithoutApprox("../tests/data/bvshl0.smt2") == SAT );
     REQUIRE( SolveWithoutApprox("../tests/data/check_bvsge_bvashr0_16bit.smt2") == UNSAT );
+    REQUIRE( SolveWithoutApprox("../tests/data/magnetic_field-node118398.smt2") == UNSAT );
 }
 
 TEST_CASE( "With variable approximations", "[variableapprox]" )
 {
     REQUIRE( SolveWithVariableApprox("../tests/data/audio_ac97_wavepcistream2.cpp.smt2", OVERAPPROXIMATION) == UNSAT );
     REQUIRE( SolveWithVariableApprox("../tests/data/jain_7_true-unreach-call_true-no-overflow.i_61.smt2", OVERAPPROXIMATION) == UNSAT );
     REQUIRE( SolveWithVariableApprox("../tests/data/RNDPRE_3_48.smt2", UNDERAPPROXIMATION) == SAT );
+    REQUIRE( SolveWithVariableApprox("../tests/data/ETCS-essentials-node3023.smt2", UNDERAPPROXIMATION) == SAT );
+    REQUIRE( SolveWithVariableApprox("../tests/data/accelerating-node2100.smt2", UNDERAPPROXIMATION) == SAT );
+    REQUIRE( SolveWithVariableApprox("../tests/data/binary_driver-2007-10-09-node11383.smt2", UNDERAPPROXIMATION) == SAT );
+    REQUIRE( SolveWithVariableApprox("../tests/data/ARI118=1.smt2", OVERAPPROXIMATION) == UNSAT );
 }
 
 TEST_CASE( "With bothLimit approximations", "[bothlimitapprox]" )