diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress0/push-pop/issue3915-real-as-int.smt2 | 33 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/real-to-int-quant.smt2 | 6 |
3 files changed, 41 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 34f7a8713..a7d931246 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -682,6 +682,7 @@ set(regress_0_tests regress0/push-pop/incremental-subst-bug.cvc regress0/push-pop/issue1986.smt2 regress0/push-pop/issue2137.min.smt2 + regress0/push-pop/issue3915-real-as-int.smt2 regress0/push-pop/quant-fun-proc-unfd.smt2 regress0/push-pop/simple_unsat_cores.smt2 regress0/push-pop/test.00.cvc @@ -1508,6 +1509,7 @@ set(regress_1_tests regress1/quantifiers/qe.smt2 regress1/quantifiers/quant-wf-int-ind.smt2 regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 + regress1/quantifiers/real-to-int-quant.smt2 regress1/quantifiers/recfact.cvc regress1/quantifiers/rel-trigger-unusable.smt2 regress1/quantifiers/repair-const-nterm.smt2 diff --git a/test/regress/regress0/push-pop/issue3915-real-as-int.smt2 b/test/regress/regress0/push-pop/issue3915-real-as-int.smt2 new file mode 100644 index 000000000..ad6ba3b33 --- /dev/null +++ b/test/regress/regress0/push-pop/issue3915-real-as-int.smt2 @@ -0,0 +1,33 @@ +; COMMAND-LINE: --incremental --check-models --solve-real-as-int
+; EXPECT: sat
+(set-logic UFNIA)
+(set-option :incremental true)
+(set-option :check-models true)
+(set-option :solve-real-as-int 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 i1 Int)
+(assert (forall ((q0 Int) (q1 Int) (q2 Int) (q3 Bool)) (=> (= v7 q3 v7 q3 v0 q3 q3 q3 q3 v3) (> q0 59))))
+(push 1)
+(declare-const v15 Bool)
+(declare-sort S0 0)
+(declare-sort S1 0)
+(declare-const i2 Int)
+(assert v13)
+(push 1)
+(declare-const S1-0 S1)
+(assert (forall ((q4 Int)) (not (distinct q4 q4))))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/real-to-int-quant.smt2 b/test/regress/regress1/quantifiers/real-to-int-quant.smt2 new file mode 100644 index 000000000..5d7b8d44e --- /dev/null +++ b/test/regress/regress1/quantifiers/real-to-int-quant.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --solve-real-as-int +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(assert (forall ((x Real) (y Real)) (=> (< x y) (exists ((z Real)) (and (< x z) (< z (+ y 2)))))) ) +(check-sat) |