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.

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)