diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-05 14:38:16 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-05 14:38:16 -0600 |
| commit | d26ee67911fedfef966a0e4d64ffda02007d65a0 (patch) | |
| tree | d8d5511eeb12ecace73845785546df95e8f67f1f /test/regress/regress0/push-pop/issue3915-real-as-int.smt2 | |
| parent | 04039407e6308070c148de0d5e93640ec1b0a341 (diff) | |
Fix issues with real to int (#3918)
This fixes a few issues in the real to int preprocessing pass. Previously it was not robust to cases where the input had constraints that were not over the reals.
Fixes #3915 and fixes #3913 and fixes #3916.
Diffstat (limited to 'test/regress/regress0/push-pop/issue3915-real-as-int.smt2')
| -rw-r--r-- | test/regress/regress0/push-pop/issue3915-real-as-int.smt2 | 33 |
1 files changed, 33 insertions, 0 deletions
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)
|