From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 12 Apr 2022 14:19:53 +0000 (-0500)
Subject: Making some benchmarks SMT-LIB compliant for subtypes (#8600)
X-Git-Tag: cvc5-1.0.1~272
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=13c3b7355c5bf0ed749f9be9b1cefb7262d08353;p=cvc5.git

Making some benchmarks SMT-LIB compliant for subtypes (#8600)

This makes some of our regressions compliant for arithmetic subtyping. This is required to make these benchmarks parsable when subtyping is eliminated.

We should discuss whether we should be permissive for such benchmarks. Regardless, the majority of our regressions should be SMT-LIB compliant.
---

diff --git a/test/regress/cli/regress0/arith/arith-mixed-types-no-tighten.smt2 b/test/regress/cli/regress0/arith/arith-mixed-types-no-tighten.smt2
index 0281805fb..120aea616 100644
--- a/test/regress/cli/regress0/arith/arith-mixed-types-no-tighten.smt2
+++ b/test/regress/cli/regress0/arith/arith-mixed-types-no-tighten.smt2
@@ -8,9 +8,9 @@
 ; Even though `n` is an integer, this would be UNSAT for real `n`, so the integrality can be ignored.
 (assert
     (and
-        (>= (+ x n) 1)
+        (>= (+ x (to_real n)) 1.0)
         (<= n 0)
-        (<= x 0)
+        (<= x 0.0)
     )
 )
 
diff --git a/test/regress/cli/regress0/arith/arith-tighten-1.smt2 b/test/regress/cli/regress0/arith/arith-tighten-1.smt2
index 8023ea0a4..fa1408536 100644
--- a/test/regress/cli/regress0/arith/arith-tighten-1.smt2
+++ b/test/regress/cli/regress0/arith/arith-tighten-1.smt2
@@ -11,8 +11,8 @@
 
 (assert (= x y))
 (assert (= x (- 2.5 y)))
-(assert (>= (+ i j) x))
-(assert (<= j (+ x 0.5)))
+(assert (>= (to_real (+ i j)) x))
+(assert (<= (to_real j) (+ x 0.5)))
 (assert (<= i 0))
 
 (check-sat)
diff --git a/test/regress/cli/regress0/arith/arith.03.cvc.smt2 b/test/regress/cli/regress0/arith/arith.03.cvc.smt2
index 777526117..a72d2648d 100644
--- a/test/regress/cli/regress0/arith/arith.03.cvc.smt2
+++ b/test/regress/cli/regress0/arith/arith.03.cvc.smt2
@@ -3,4 +3,4 @@
 (set-option :incremental false)
 (declare-fun x () Real)
 (declare-fun y () Real)
-(check-sat-assuming ( (not (let ((_let_1 (+ x y))) (= (* _let_1 _let_1) (+ (+ (* x x) (* (* 2 x) y)) (* y y))))) ))
+(check-sat-assuming ( (not (let ((_let_1 (+ x y))) (= (* _let_1 _let_1) (+ (+ (* x x) (* (* 2.0 x) y)) (* y y))))) ))
diff --git a/test/regress/cli/regress0/arith/bug549.cvc.smt2 b/test/regress/cli/regress0/arith/bug549.cvc.smt2
index 74bdc8878..8a62b7064 100644
--- a/test/regress/cli/regress0/arith/bug549.cvc.smt2
+++ b/test/regress/cli/regress0/arith/bug549.cvc.smt2
@@ -3,4 +3,4 @@
 (set-option :incremental false)
 (declare-fun a () Real)
 (declare-fun b () Real)
-(check-sat-assuming ( (not (= (^ (* a b) 5) (* (* (* (* (* (* (* (* (* b a) a) a) a) b) b) b) b) a))) ))
+(check-sat-assuming ( (not (= (^ (* a b) 5.0) (* (* (* (* (* (* (* (* (* b a) a) a) a) b) b) b) b) a))) ))
diff --git a/test/regress/cli/regress0/arith/bug569.smt2 b/test/regress/cli/regress0/arith/bug569.smt2
index 99bedad3a..f436ca0e8 100644
--- a/test/regress/cli/regress0/arith/bug569.smt2
+++ b/test/regress/cli/regress0/arith/bug569.smt2
@@ -9,7 +9,7 @@
 (declare-fun v3 () Int)
 (declare-fun v5 () Real)
 (assert (= (to_real v1) (+ (to_real v3) v5)))
-(assert (< v5 1))
-(assert (> v5 0))
+(assert (< v5 1.0))
+(assert (> v5 0.0))
 (check-sat)
 (exit)
diff --git a/test/regress/cli/regress0/arith/issue3683.smt2 b/test/regress/cli/regress0/arith/issue3683.smt2
index 0ce6dc89d..60492ea09 100644
--- a/test/regress/cli/regress0/arith/issue3683.smt2
+++ b/test/regress/cli/regress0/arith/issue3683.smt2
@@ -1,5 +1,5 @@
 (set-logic ALL)
 (declare-fun a () Real)
-(assert (= (+ 2 (exp (+ 2 a))) 0))
+(assert (= (+ 2.0 (exp (+ 2.0 a))) 0.0))
 (set-info :status unsat)
 (check-sat)
diff --git a/test/regress/cli/regress0/arith/issue8159-rewrite-intreal.smt2 b/test/regress/cli/regress0/arith/issue8159-rewrite-intreal.smt2
index a15191115..c204ca0de 100644
--- a/test/regress/cli/regress0/arith/issue8159-rewrite-intreal.smt2
+++ b/test/regress/cli/regress0/arith/issue8159-rewrite-intreal.smt2
@@ -2,5 +2,5 @@
 (set-logic QF_LIRA)
 (declare-fun a () Real)
 (declare-fun b () Int)
-(assert (>= a (+ a b)))
+(assert (>= a (+ a (to_real b))))
 (check-sat)
diff --git a/test/regress/cli/regress0/cores/issue3455.smt2 b/test/regress/cli/regress0/cores/issue3455.smt2
index b922bb7fa..c07fc5541 100644
--- a/test/regress/cli/regress0/cores/issue3455.smt2
+++ b/test/regress/cli/regress0/cores/issue3455.smt2
@@ -6,11 +6,11 @@
 ; EXPECT: unsat
 (declare-fun x0 () Real)
 (check-sat)
-(assert (<= (* x0 (- 1)) 0))
-(assert (or (>= 0 x0) (> (+ 1.0 x0) (- 12))))
+(assert (<= (* x0 (- 1.0)) 0.0))
+(assert (or (>= 0.0 x0) (> (+ 1.0 x0) (- 12.0))))
 (check-sat)
 (push)
-(assert (<= x0 (- 13)))
+(assert (<= x0 (- 13.0)))
 (check-sat)
 (check-sat)
 (check-sat)
diff --git a/test/regress/cli/regress0/cores/issue3651.smt2 b/test/regress/cli/regress0/cores/issue3651.smt2
index 104767439..478f198ab 100644
--- a/test/regress/cli/regress0/cores/issue3651.smt2
+++ b/test/regress/cli/regress0/cores/issue3651.smt2
@@ -7,15 +7,15 @@
 (declare-fun a () Real)
 (declare-fun b () Real)
 (declare-fun c () Real)
-(assert (> (+ (/ (- 2) a) (* 8 a)) 0))
-(assert (<= b 0))
-(assert (= (+ (* 4 a) (* 2 b)) 1))
-(assert (>= (* b c) 0))
+(assert (> (+ (/ (- 2.0) a) (* 8.0 a)) 0.0))
+(assert (<= b 0.0))
+(assert (= (+ (* 4.0 a) (* 2.0 b)) 1.0))
+(assert (>= (* b c) 0.0))
 (check-sat)
 (check-sat)
 (check-sat)
 (push)
 (check-sat)
 (pop)
-(assert (>= c 1))
+(assert (>= c 1.0))
 (check-sat)
diff --git a/test/regress/cli/regress0/cores/issue5079.smt2 b/test/regress/cli/regress0/cores/issue5079.smt2
index cc828deb1..db3137692 100644
--- a/test/regress/cli/regress0/cores/issue5079.smt2
+++ b/test/regress/cli/regress0/cores/issue5079.smt2
@@ -6,11 +6,11 @@
 (declare-fun a () Real)
 (declare-fun b () Real)
 (assert (<= b 0.25))
-(assert (= (- b a) 3))
-(assert (or (> (* 2 b) 0) (= (/ 1 b) 3)))
+(assert (= (- b a) 3.0))
+(assert (or (> (* 2 b) 0.0) (= (/ 1.0 b) 3.0)))
 (check-sat)
 (push)
 (check-sat)
 (pop)
-(assert (>= (* 3 a) 1))
-(check-sat)
\ No newline at end of file
+(assert (>= (* 3.0 a) 1.0))
+(check-sat)
diff --git a/test/regress/cli/regress0/cores/issue5238.smt2 b/test/regress/cli/regress0/cores/issue5238.smt2
index 765bcdc2c..27bfac37c 100644
--- a/test/regress/cli/regress0/cores/issue5238.smt2
+++ b/test/regress/cli/regress0/cores/issue5238.smt2
@@ -5,10 +5,10 @@
 (set-logic ALL)
 (declare-fun a () Real)
 (declare-fun b () Real)
-(assert (distinct b 0))
-(assert (= b 2))
-(assert (= (/ 0 a) 1))
+(assert (distinct b 0.0))
+(assert (= b 2.0))
+(assert (= (/ 0.0 a) 1.0))
 (check-sat)
-(assert (= (+ a b) 0))
-(check-sat-assuming ((> b 1)))
+(assert (= (+ a b) 0.0))
+(check-sat-assuming ((> b 1.0)))
 (check-sat)
diff --git a/test/regress/cli/regress0/cvc3-bug15.cvc.smt2 b/test/regress/cli/regress0/cvc3-bug15.cvc.smt2
index e7566d495..ef61be474 100644
--- a/test/regress/cli/regress0/cvc3-bug15.cvc.smt2
+++ b/test/regress/cli/regress0/cvc3-bug15.cvc.smt2
@@ -5,6 +5,6 @@
 (declare-fun y () Real)
 (declare-fun f (Real) Real)
 (assert (=> (> x y) (> (f x) (f y))))
-(assert (= x 3))
-(assert (= y 2))
+(assert (= x 3.0))
+(assert (= y 2.0))
 (check-sat-assuming ( (not (> (f x) (f y))) ))
diff --git a/test/regress/cli/regress0/datatypes/pair-real-bool.smt2 b/test/regress/cli/regress0/datatypes/pair-real-bool.smt2
index f8ed3dd3c..566367179 100644
--- a/test/regress/cli/regress0/datatypes/pair-real-bool.smt2
+++ b/test/regress/cli/regress0/datatypes/pair-real-bool.smt2
@@ -21,6 +21,6 @@
 (declare-const result (Pair Real Bool))
 (assert (= l1 (Node l2 5.0 l2)))
 (assert (= result (SumeAndPositiveTree l1)))
-(assert (= (first result) 5))
+(assert (= (first result) 5.0))
 (assert (= (second result) true))
 (check-sat)
diff --git a/test/regress/cli/regress0/fmf/syn002-si-real-int.smt2 b/test/regress/cli/regress0/fmf/syn002-si-real-int.smt2
index 1e72650c2..626f98469 100644
--- a/test/regress/cli/regress0/fmf/syn002-si-real-int.smt2
+++ b/test/regress/cli/regress0/fmf/syn002-si-real-int.smt2
@@ -6,6 +6,6 @@
 (declare-fun $$rtu (Real) $$unsorted)
 (declare-fun $$utr ($$unsorted) Real)
 (declare-fun p ($$unsorted) Bool)
-(assert (and (= ($$utr ($$rtu 12)) 12) (= ($$utr ($$rtu (/ 41 152))) (/ 41 152)) ))
+(assert (and (= ($$utr ($$rtu 12.0)) 12.0) (= ($$utr ($$rtu (/ 41 152))) (/ 41 152)) ))
 (assert (forall ((x $$unsorted)) (p x)))
 (check-sat)
diff --git a/test/regress/cli/regress0/fp/issue4277-assign-func.smt2 b/test/regress/cli/regress0/fp/issue4277-assign-func.smt2
index d1fbc73d2..33753375f 100644
--- a/test/regress/cli/regress0/fp/issue4277-assign-func.smt2
+++ b/test/regress/cli/regress0/fp/issue4277-assign-func.smt2
@@ -6,5 +6,5 @@
 (declare-fun b () (_ BitVec 1))
 (declare-fun c () (_ BitVec 8))
 (declare-fun d () (_ BitVec 23))
-(assert (= 0 (fp.to_real (fp b c d))))
+(assert (= 0.0 (fp.to_real (fp b c d))))
 (check-sat)
diff --git a/test/regress/cli/regress0/fp/issue5734.smt2 b/test/regress/cli/regress0/fp/issue5734.smt2
index d66e6aec7..832b1c9b9 100644
--- a/test/regress/cli/regress0/fp/issue5734.smt2
+++ b/test/regress/cli/regress0/fp/issue5734.smt2
@@ -2,5 +2,5 @@
 (set-logic QF_FP)
 (declare-fun a () RoundingMode)
 (declare-fun b () (_ FloatingPoint 8 24))
-(assert (= b (fp.add a b (fp.add a ((_ to_fp 8 24) a ((_ to_fp 8 24) a 0)) b))))
+(assert (= b (fp.add a b (fp.add a ((_ to_fp 8 24) a ((_ to_fp 8 24) a 0.0)) b))))
 (check-sat)
diff --git a/test/regress/cli/regress0/fp/issue7569.smt2 b/test/regress/cli/regress0/fp/issue7569.smt2
index c4bffc3da..01b9aa53c 100644
--- a/test/regress/cli/regress0/fp/issue7569.smt2
+++ b/test/regress/cli/regress0/fp/issue7569.smt2
@@ -2,6 +2,6 @@
 (declare-const X (_ FloatingPoint 8 24))
 (declare-const R Real)
 (assert (= X ((_ to_fp 8 24) RTZ (- R))))
-(assert (= X ((_ to_fp 8 24) RTZ 0)))
+(assert (= X ((_ to_fp 8 24) RTZ 0.0)))
 (set-info :status sat)
 (check-sat)
diff --git a/test/regress/cli/regress0/get-value-reals-ints.smt2 b/test/regress/cli/regress0/get-value-reals-ints.smt2
index 8951cc797..7834ed581 100644
--- a/test/regress/cli/regress0/get-value-reals-ints.smt2
+++ b/test/regress/cli/regress0/get-value-reals-ints.smt2
@@ -15,11 +15,11 @@
 (declare-fun neg_int () Int)
 
 (assert (= pos_int 5))
-(assert (= pos_real_int_value 3))
+(assert (= pos_real_int_value 3.0))
 (assert (= pos_rat (/ 1 3)))
-(assert (= zero 0))
+(assert (= zero 0.0))
 (assert (= neg_rat (/ (- 2) 3)))
-(assert (= neg_real_int_value (- 2)))
+(assert (= neg_real_int_value (- 2.0)))
 (assert (= neg_int (- 6)))
 
 (check-sat)
diff --git a/test/regress/cli/regress0/ho/issue5744-cg-model.smt2 b/test/regress/cli/regress0/ho/issue5744-cg-model.smt2
index 5650351cd..e99f677b0 100644
--- a/test/regress/cli/regress0/ho/issue5744-cg-model.smt2
+++ b/test/regress/cli/regress0/ho/issue5744-cg-model.smt2
@@ -2,6 +2,6 @@
 (set-info :status sat)
 (declare-fun r4 () Real)
 (declare-fun ufrb5 (Real Real Real Real Real) Bool)
-(assert (ufrb5 0.0 0.0 0.0 0.0 0))
-(assert (ufrb5 (+ r4 r4) 0.0 1 0.0 0.0))
+(assert (ufrb5 0.0 0.0 0.0 0.0 0.0))
+(assert (ufrb5 (+ r4 r4) 0.0 1.0 0.0 0.0))
 (check-sat)
diff --git a/test/regress/cli/regress0/nl/issue3475.smt2 b/test/regress/cli/regress0/nl/issue3475.smt2
index 092e8513f..a83e60c19 100644
--- a/test/regress/cli/regress0/nl/issue3475.smt2
+++ b/test/regress/cli/regress0/nl/issue3475.smt2
@@ -2,7 +2,7 @@
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun x () Real)
-(assert (< x 0))
+(assert (< x 0.0))
 (assert (not (= (/ (sqrt x) (sqrt x)) x)))
 (set-info :status sat)
 (check-sat)
diff --git a/test/regress/cli/regress0/nl/nta/issue4693-5-inc-purify.smt2 b/test/regress/cli/regress0/nl/nta/issue4693-5-inc-purify.smt2
index 730db4b23..9acc326d0 100644
--- a/test/regress/cli/regress0/nl/nta/issue4693-5-inc-purify.smt2
+++ b/test/regress/cli/regress0/nl/nta/issue4693-5-inc-purify.smt2
@@ -2,5 +2,5 @@
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)
-(assert (forall ((t Real)) (= 0 (/ t (cos 1.0)))))
+(assert (forall ((t Real)) (= 0.0 (/ t (cos 1.0)))))
 (check-sat)
diff --git a/test/regress/cli/regress0/nl/nta/issue7938-tf-model.smt2 b/test/regress/cli/regress0/nl/nta/issue7938-tf-model.smt2
index eff66c77d..75dbf0ac3 100644
--- a/test/regress/cli/regress0/nl/nta/issue7938-tf-model.smt2
+++ b/test/regress/cli/regress0/nl/nta/issue7938-tf-model.smt2
@@ -5,5 +5,5 @@
 (declare-const x5 Real)
 (declare-fun s () Real)
 (assert (exists ((S Real)) (= s (sin 1.0))))
-(assert (xor (and (= 0.0 (/ x5 0.0)) (= x (- 0.0 1 (/ 0.0 x))) (= x 1)) x3))
+(assert (xor (and (= 0.0 (/ x5 0.0)) (= x (- 0.0 1.0 (/ 0.0 x))) (= x 1.0)) x3))
 (check-sat)
diff --git a/test/regress/cli/regress0/nl/nta/issue8147-unc-model.smt2 b/test/regress/cli/regress0/nl/nta/issue8147-unc-model.smt2
index 1acdab13b..20f0a6190 100644
--- a/test/regress/cli/regress0/nl/nta/issue8147-unc-model.smt2
+++ b/test/regress/cli/regress0/nl/nta/issue8147-unc-model.smt2
@@ -4,5 +4,5 @@
 (declare-fun a () Real)
 (declare-fun r () Real)
 (declare-fun v () Real)
-(assert (and (xor (= a 1.0) x) (= 1 (- v (exp (* r v))))))
+(assert (and (xor (= a 1.0) x) (= 1.0 (- v (exp (* r v))))))
 (check-sat)
diff --git a/test/regress/cli/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2 b/test/regress/cli/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
index 13088e551..c74d7ad6a 100644
--- a/test/regress/cli/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
+++ b/test/regress/cli/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
@@ -4,5 +4,5 @@
 (set-info :status sat)
 (declare-fun a () Real)
 (declare-fun b () Real)
-(assert (= a (* b (+ (sin a) (/ 1 a)))))
+(assert (= a (* b (+ (sin a) (/ 1.0 a)))))
 (check-sat)
diff --git a/test/regress/cli/regress0/nl/nta/issue8182-exact-mv-keep.smt2 b/test/regress/cli/regress0/nl/nta/issue8182-exact-mv-keep.smt2
index 0d71007ac..abeb65ba4 100644
--- a/test/regress/cli/regress0/nl/nta/issue8182-exact-mv-keep.smt2
+++ b/test/regress/cli/regress0/nl/nta/issue8182-exact-mv-keep.smt2
@@ -2,6 +2,6 @@
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun v () Real)
-(assert (forall ((V Real)) (> 0 (/ 0.0 v))))
+(assert (forall ((V Real)) (> 0.0 (/ 0.0 v))))
 (assert (= 0.0 (* (sin v) (sin 1.0))))
 (check-sat)
diff --git a/test/regress/cli/regress0/nl/nta/issue8183-tc-pi.smt2 b/test/regress/cli/regress0/nl/nta/issue8183-tc-pi.smt2
index 40fa6154f..37ff9de18 100644
--- a/test/regress/cli/regress0/nl/nta/issue8183-tc-pi.smt2
+++ b/test/regress/cli/regress0/nl/nta/issue8183-tc-pi.smt2
@@ -4,5 +4,5 @@
 (set-info :status sat)
 (declare-fun v () Real)
 (declare-fun a () (Array Real Real))
-(assert (exists ((V Real)) (or (and (= 0 (/ 0 v)) (< 0 (/ 0 v))) (= 1.0 (select (store a (/ (+ 0.0 real.pi) 0.0) 0.0) 0.0)))))
+(assert (exists ((V Real)) (or (and (= 0.0 (/ 0.0 v)) (< 0.0 (/ 0.0 v))) (= 1.0 (select (store a (/ (+ 0.0 real.pi) 0.0) 0.0) 0.0)))))
 (check-sat)
diff --git a/test/regress/cli/regress0/nl/nta/issue8415-embed-arg.smt2 b/test/regress/cli/regress0/nl/nta/issue8415-embed-arg.smt2
index 1be656f19..0b24adb7e 100644
--- a/test/regress/cli/regress0/nl/nta/issue8415-embed-arg.smt2
+++ b/test/regress/cli/regress0/nl/nta/issue8415-embed-arg.smt2
@@ -2,5 +2,5 @@
 (set-info :status unsat)
 (declare-fun r8 () Real)
 (declare-fun v57 () Bool)
-(assert (and (= 0.0 (exp (exp (+ 1.0 1.0)))) (not (= 0 (* r8 (ite v57 1 0))))))
+(assert (and (= 0.0 (exp (exp (+ 1.0 1.0)))) (not (= 0.0 (* r8 (ite v57 1.0 0.0))))))
 (check-sat)
diff --git a/test/regress/cli/regress0/nl/real-as-int.smt2 b/test/regress/cli/regress0/nl/real-as-int.smt2
index 9599b6e6b..8f7f2e535 100644
--- a/test/regress/cli/regress0/nl/real-as-int.smt2
+++ b/test/regress/cli/regress0/nl/real-as-int.smt2
@@ -4,7 +4,7 @@
 (set-info :status sat)
 (declare-fun a () Real)
 (declare-fun b () Real)
-(assert (= (* a a) 4))
-(assert (= (* b b) 0))
-(assert (= (+ (* a a) (* b b)) 4))
+(assert (= (* a a) 4.0))
+(assert (= (* b b) 0.0))
+(assert (= (+ (* a a) (* b b)) 4.0))
 (check-sat)
diff --git a/test/regress/cli/regress0/nl/sqrt.smt2 b/test/regress/cli/regress0/nl/sqrt.smt2
index 92c4dabba..ba760bf88 100644
--- a/test/regress/cli/regress0/nl/sqrt.smt2
+++ b/test/regress/cli/regress0/nl/sqrt.smt2
@@ -27,7 +27,7 @@
 (pop)
 
 (push)
-(assert (< x 0))
+(assert (< x 0.0))
 (assert (= (sqrt 1.0) (sqrt x)))
 (check-sat)
 (pop)
diff --git a/test/regress/cli/regress0/nl/tpp-fail-pf-012921.smt2 b/test/regress/cli/regress0/nl/tpp-fail-pf-012921.smt2
index c97a12074..b6a745917 100644
--- a/test/regress/cli/regress0/nl/tpp-fail-pf-012921.smt2
+++ b/test/regress/cli/regress0/nl/tpp-fail-pf-012921.smt2
@@ -1,5 +1,5 @@
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun x () Real)
-(assert (and (> 0.0 x) (not (= 0.0 (/ 0.0 (* 2 x))))))
+(assert (and (> 0.0 x) (not (= 0.0 (/ 0.0 (* 2.0 x))))))
 (check-sat)
diff --git a/test/regress/cli/regress0/precedence/plus-mult.cvc.smt2 b/test/regress/cli/regress0/precedence/plus-mult.cvc.smt2
index 1b2711597..e8a0dafd9 100644
--- a/test/regress/cli/regress0/precedence/plus-mult.cvc.smt2
+++ b/test/regress/cli/regress0/precedence/plus-mult.cvc.smt2
@@ -6,4 +6,4 @@
 (declare-fun c () Int)
 (declare-fun d () Int)
 (declare-fun e () Int)
-(check-sat-assuming ( (not (let ((_let_1 (- (+ (- (+ a (/ (* 2 b) 3)) (* (/ c 4) 5)) (/ d 6)) e))) (= _let_1 _let_1))) ))
+(check-sat-assuming ( (not (let ((_let_1 (- (+ (- (+ (to_real a) (/ (* 2 b) 3)) (* (/ c 4) 5.0)) (/ d 6)) (to_real e)))) (= _let_1 _let_1))) ))
diff --git a/test/regress/cli/regress0/preprocess/preprocess_10.cvc.smt2 b/test/regress/cli/regress0/preprocess/preprocess_10.cvc.smt2
index f928a51e7..a41fb0cdd 100644
--- a/test/regress/cli/regress0/preprocess/preprocess_10.cvc.smt2
+++ b/test/regress/cli/regress0/preprocess/preprocess_10.cvc.smt2
@@ -3,6 +3,6 @@
 (set-option :incremental false)
 (declare-fun x () Real)
 (declare-fun b () Bool)
-(assert (= x (ite b 10 (- 10))))
+(assert (= x (ite b 10.0 (- 10.0))))
 (assert b)
 (check-sat)
diff --git a/test/regress/cli/regress0/preprocess/preprocess_11.cvc.smt2 b/test/regress/cli/regress0/preprocess/preprocess_11.cvc.smt2
index 6cb631b6b..09893f57e 100644
--- a/test/regress/cli/regress0/preprocess/preprocess_11.cvc.smt2
+++ b/test/regress/cli/regress0/preprocess/preprocess_11.cvc.smt2
@@ -3,5 +3,5 @@
 (set-option :incremental false)
 (declare-fun x () Real)
 (declare-fun y () Real)
-(assert (and (and (and (= 0 (ite true x 1)) (= 0 (ite (= x 0) 0 1))) (= x (ite true y 0))) (= 0 (ite true 0 0))))
+(assert (and (and (and (= 0.0 (ite true x 1.0)) (= 0.0 (ite (= x 0.0) 0.0 1.0))) (= x (ite true y 0.0))) (= 0.0 (ite true 0.0 0.0))))
 (check-sat)
diff --git a/test/regress/cli/regress0/preprocess/preprocess_12.cvc.smt2 b/test/regress/cli/regress0/preprocess/preprocess_12.cvc.smt2
index c1fd76ad5..cc2966bab 100644
--- a/test/regress/cli/regress0/preprocess/preprocess_12.cvc.smt2
+++ b/test/regress/cli/regress0/preprocess/preprocess_12.cvc.smt2
@@ -4,5 +4,5 @@
 (declare-fun x () Real)
 (declare-fun y () Real)
 (declare-fun b () Bool)
-(assert (= 0 (ite b (- x y) (* 2 x))))
+(assert (= 0.0 (ite b (- x y) (* 2.0 x))))
 (check-sat)
diff --git a/test/regress/cli/regress0/quantifiers/is-int.smt2 b/test/regress/cli/regress0/quantifiers/is-int.smt2
index fc7fbb180..4ea5d91e1 100644
--- a/test/regress/cli/regress0/quantifiers/is-int.smt2
+++ b/test/regress/cli/regress0/quantifiers/is-int.smt2
@@ -1,4 +1,4 @@
 (set-logic LIRA)
 (set-info :status unsat)
-(assert (forall ((X Real) (Y Real)) (or (not (is_int X)) (not (>= (+ X (* (- (/ 2 3)) Y)) (- (/ 1 6)))) (not (>= (+ (* (- 1) X) (* (- (/ 1 4)) Y)) (- (/ 61 8)))) (not (>= (+ (* (- 1) X) (* (/ 5 2) Y)) 13))) ))
-(check-sat)
\ No newline at end of file
+(assert (forall ((X Real) (Y Real)) (or (not (is_int X)) (not (>= (+ X (* (- (/ 2 3)) Y)) (- (/ 1 6)))) (not (>= (+ (* (- 1.0) X) (* (- (/ 1 4)) Y)) (- (/ 61 8)))) (not (>= (+ (* (- 1.0) X) (* (/ 5 2) Y)) 13.0))) ))
+(check-sat)
diff --git a/test/regress/cli/regress0/quantifiers/issue4086-infs.smt2 b/test/regress/cli/regress0/quantifiers/issue4086-infs.smt2
index 432218e73..3cd026fdf 100644
--- a/test/regress/cli/regress0/quantifiers/issue4086-infs.smt2
+++ b/test/regress/cli/regress0/quantifiers/issue4086-infs.smt2
@@ -3,5 +3,5 @@
 (set-option :cegqi-inf-int true)
 (set-option :cegqi-inf-real true)
 (set-option :var-ineq-elim-quant false) 
-(assert (forall (( b Real )) (forall (( c Int )) (and  (> c (* b 2 ))))))
+(assert (forall (( b Real )) (forall (( c Int )) (and  (> (to_real c) (* b 2.0))))))
 (check-sat)    
diff --git a/test/regress/cli/regress0/quantifiers/macros-real-arg.smt2 b/test/regress/cli/regress0/quantifiers/macros-real-arg.smt2
index 52eeedae6..770402ad9 100644
--- a/test/regress/cli/regress0/quantifiers/macros-real-arg.smt2
+++ b/test/regress/cli/regress0/quantifiers/macros-real-arg.smt2
@@ -8,5 +8,5 @@
 (declare-fun k () Real)
 (declare-fun k2 () Int)
 (assert (or (not (P (to_int k))) (not (P k2))))
-(assert (= k 0))
+(assert (= k 0.0))
 (check-sat)
diff --git a/test/regress/cli/regress0/quantifiers/mix-match.smt2 b/test/regress/cli/regress0/quantifiers/mix-match.smt2
index 9329f4c56..d123bf9c4 100644
--- a/test/regress/cli/regress0/quantifiers/mix-match.smt2
+++ b/test/regress/cli/regress0/quantifiers/mix-match.smt2
@@ -3,7 +3,7 @@
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun P (Real) Bool)
-(assert (forall ((x Int)) (P x)))
+(assert (forall ((x Int)) (P (to_real x))))
 
 (declare-fun a () Real)
 (assert (is_int a))
diff --git a/test/regress/cli/regress0/quantifiers/mix-simp.smt2 b/test/regress/cli/regress0/quantifiers/mix-simp.smt2
index feda11740..cb57097ce 100644
--- a/test/regress/cli/regress0/quantifiers/mix-simp.smt2
+++ b/test/regress/cli/regress0/quantifiers/mix-simp.smt2
@@ -2,5 +2,5 @@
 ; EXPECT: sat
 (set-logic LIRA)
 (set-info :status sat)
-(assert (forall ((x Real)) (exists ((y Int)) (and (>= y x) (< y (+ x 1))))))
+(assert (forall ((x Real)) (exists ((y Int)) (and (>= (to_real y) x) (< (to_real y) (+ x 1.0))))))
 (check-sat)
diff --git a/test/regress/cli/regress0/quantifiers/simp-typ-test.smt2 b/test/regress/cli/regress0/quantifiers/simp-typ-test.smt2
index 380a66aac..7e1b53ca0 100644
--- a/test/regress/cli/regress0/quantifiers/simp-typ-test.smt2
+++ b/test/regress/cli/regress0/quantifiers/simp-typ-test.smt2
@@ -3,5 +3,5 @@
 ; ensure that E-matching matches on sub-types
 (declare-fun P (Real) Bool)
 (assert (forall ((x Real)) (P x)))
-(assert (not (P 5)))
-(check-sat)
\ No newline at end of file
+(assert (not (P 5.0)))
+(check-sat)
diff --git a/test/regress/cli/regress0/smtlib/reset-assertions2.smt2 b/test/regress/cli/regress0/smtlib/reset-assertions2.smt2
index 3c37f2cba..be00967b4 100644
--- a/test/regress/cli/regress0/smtlib/reset-assertions2.smt2
+++ b/test/regress/cli/regress0/smtlib/reset-assertions2.smt2
@@ -8,7 +8,7 @@
 (declare-fun y () Real)
 (assert (> x 0.0))
 (assert (> y 0.0))
-(assert (= (+ (* 2 x) y) 4))
+(assert (= (+ (* 2.0 x) y) 4.0))
 (check-sat)
 (reset-assertions)
 
diff --git a/test/regress/cli/regress0/uflra/bug293.cvc.smt2 b/test/regress/cli/regress0/uflra/bug293.cvc.smt2
index c3070ed06..a0a8f715e 100644
--- a/test/regress/cli/regress0/uflra/bug293.cvc.smt2
+++ b/test/regress/cli/regress0/uflra/bug293.cvc.smt2
@@ -3,7 +3,7 @@
 (set-option :incremental false)
 (declare-fun x () Real)
 (declare-fun f (Real) Real)
-(assert (not (= (f 1) (f x))))
-(assert (not (= (f 0) (f x))))
-(assert (xor (= x 0) (= x 1)))
+(assert (not (= (f 1.0) (f x))))
+(assert (not (= (f 0.0) (f x))))
+(assert (xor (= x 0.0) (= x 1.0)))
 (check-sat)
diff --git a/test/regress/cli/regress0/unconstrained/arith2.smt2 b/test/regress/cli/regress0/unconstrained/arith2.smt2
index d664647a5..9329eea55 100644
--- a/test/regress/cli/regress0/unconstrained/arith2.smt2
+++ b/test/regress/cli/regress0/unconstrained/arith2.smt2
@@ -6,8 +6,8 @@
 (declare-fun v1 () Int)
 (declare-fun v2 () Int)
 (declare-fun v3 () Real)
-(assert (= (+ v1 v2) v3))
-(assert (< v3 v2))
-(assert (> v3 (- v2 1)))
+(assert (= (to_real (+ v1 v2)) v3))
+(assert (< v3 (to_real v2)))
+(assert (> v3 (to_real (- v2 1))))
 (check-sat)
 (exit)
diff --git a/test/regress/cli/regress0/unconstrained/arith4.smt2 b/test/regress/cli/regress0/unconstrained/arith4.smt2
index 5bb5f1eee..286b5978d 100644
--- a/test/regress/cli/regress0/unconstrained/arith4.smt2
+++ b/test/regress/cli/regress0/unconstrained/arith4.smt2
@@ -8,8 +8,8 @@
 (declare-fun v3 () Int)
 (declare-fun v4 () Int)
 (declare-fun v5 () Real)
-(assert (= (* v1 v2) (+ (* v3 v4) v5)))
-(assert (< v5 1))
-(assert (> v5 0))
+(assert (= (to_real (* v1 v2)) (+ (to_real (* v3 v4)) v5)))
+(assert (< v5 1.0))
+(assert (> v5 0.0))
 (check-sat)
 (exit)
diff --git a/test/regress/cli/regress0/unconstrained/arith7.smt2 b/test/regress/cli/regress0/unconstrained/arith7.smt2
index 4ed0aa17f..a88f8c316 100644
--- a/test/regress/cli/regress0/unconstrained/arith7.smt2
+++ b/test/regress/cli/regress0/unconstrained/arith7.smt2
@@ -5,8 +5,8 @@
 (set-info :status unsat)
 (declare-fun v1 () Int)
 (declare-fun v2 () Real)
-(assert (= (/ v1 2) v2))
+(assert (= (/ (to_real v1) 2.0) v2))
 (assert (< v2 (/ 1 2)))
-(assert (> v2 0))
+(assert (> v2 0.0))
 (check-sat)
 (exit)
diff --git a/test/regress/cli/regress1/issue7937-difficulty-irr.smt2 b/test/regress/cli/regress1/issue7937-difficulty-irr.smt2
index a18dc82f9..ae1fccf6d 100644
--- a/test/regress/cli/regress1/issue7937-difficulty-irr.smt2
+++ b/test/regress/cli/regress1/issue7937-difficulty-irr.smt2
@@ -4,5 +4,5 @@
 (declare-const x Bool)
 (declare-fun a () Real)
 (declare-fun r () Real)
-(assert (xor (= 0 (/ 0 a)) (and x (= 0.0 (/ r a r)))))
+(assert (xor (= 0.0 (/ 0.0 a)) (and x (= 0.0 (/ r a r)))))
 (check-sat)
diff --git a/test/regress/cli/regress1/nl/issue3617.smt2 b/test/regress/cli/regress1/nl/issue3617.smt2
index 149b6a535..9c3ac01b9 100644
--- a/test/regress/cli/regress1/nl/issue3617.smt2
+++ b/test/regress/cli/regress1/nl/issue3617.smt2
@@ -6,5 +6,5 @@
 (assert
 (let ((_let_0 (dbz 0.0))) (let ((_let_1 (= b 0.0))) (let ((_let_2 (/ 1.0 a))) (let ((_let_3 (dbz 1.0))) (let ((_let_4 (= a 0.0))) (let ((_let_5 (ite _let_4 _let_3 _let_2))) (let ((_let_6 (/ _let_5 b))) (let ((_let_7 (dbz _let_5))) (let ((_let_8 (dbz (dbz (ite _let_1 _let_7 _let_6))))) (or (>= (* (- 1.0) (ite (= _let_8 0.0) _let_0 (/ 0.0 _let_8))) 0.0) (>= _let_0 0.0)))))))))))
 )
-(assert (> a 0))
+(assert (> a 0.0))
 (check-sat)
diff --git a/test/regress/cli/regress1/nl/issue3803-nl-check-model.smt2 b/test/regress/cli/regress1/nl/issue3803-nl-check-model.smt2
index 545ea3e67..cd114e31c 100644
--- a/test/regress/cli/regress1/nl/issue3803-nl-check-model.smt2
+++ b/test/regress/cli/regress1/nl/issue3803-nl-check-model.smt2
@@ -7,6 +7,6 @@
 (declare-fun c () Real)
 (declare-fun d () Real)
 (declare-fun e () Real)
-(assert (exists ((f Real)) (and (or (> (+ d (* (/ (* c e) (- (* c e) e)) f)) 0 (/ 0 a))) (> e 6))))
+(assert (exists ((f Real)) (and (or (> (+ d (* (/ (* c e) (- (* c e) e)) f)) 0.0 (/ 0.0 a))) (> e 6.0))))
 (assert (distinct a (/ b e)))
 (check-sat)
diff --git a/test/regress/cli/regress1/nl/pinto-model-core-ni.smt2 b/test/regress/cli/regress1/nl/pinto-model-core-ni.smt2
index 1e09f8439..9054735c8 100644
--- a/test/regress/cli/regress1/nl/pinto-model-core-ni.smt2
+++ b/test/regress/cli/regress1/nl/pinto-model-core-ni.smt2
@@ -12,11 +12,11 @@
 (assert (>= n 1))
 (assert (and (<= 1 x)(<= x n)))
 (assert (and (<= 1 y)(<= y n)))
-(assert (or (= (/ (* (- 1) x) n) i1)(= i1 (/ x n))))
-(assert (or (= (/ (* (- 1) y) n) i2)(= i2 (/ y n))))
+(assert (or (= (/ (to_real (* (- 1) x)) (to_real n)) i1)(= i1 (/ (to_real x) (to_real n)))))
+(assert (or (= (/ (to_real (* (- 1) y)) (to_real n)) i2)(= i2 (/ (to_real y) (to_real n)))))
 
 (assert (and (= i1 i11) (= i2 i21) ))
 
-(assert (not (and (or (= (- 1) i11 )(= i11 1)) (or (= (- 1) i21)(= i21 1)) )))
+(assert (not (and (or (= (- 1.0) i11 )(= i11 1.0)) (or (= (- 1.0) i21)(= i21 1.0)) )))
 
 (check-sat)
diff --git a/test/regress/cli/regress1/nl/proj-issue215.smt2 b/test/regress/cli/regress1/nl/proj-issue215.smt2
index 24951890e..6b1d6724d 100644
--- a/test/regress/cli/regress1/nl/proj-issue215.smt2
+++ b/test/regress/cli/regress1/nl/proj-issue215.smt2
@@ -8,5 +8,5 @@
 (declare-fun g () Real)
 (assert (= (* c f c) a (- d f)))
 (assert (= d (/ a f)))
-(assert (distinct f 0 (/ b g) g))
+(assert (distinct f 0.0 (/ b g) g))
 (check-sat)
diff --git a/test/regress/cli/regress1/nl/proj-issue232.smt2 b/test/regress/cli/regress1/nl/proj-issue232.smt2
index bf8a7bcce..9f5595c77 100644
--- a/test/regress/cli/regress1/nl/proj-issue232.smt2
+++ b/test/regress/cli/regress1/nl/proj-issue232.smt2
@@ -4,16 +4,16 @@
 (assert
  (<
  (* a
-  (/ 1
-  (/ (- 2) a
+  (/ 1.0
+  (/ (- 2.0) a
    (- a
    (* a
-    (mod (to_int a)
+    (to_real (mod (to_int a)
     (to_int
      (/ a
      (* a
-      (div (to_int (/ (- 9) 800))
-      (to_int (/ a a))))))))))))
+      (to_real (div (to_int (/ (- 9) 800))
+      (to_int (/ a a))))))))))))))
  (- a)))
-(assert (<= 0 a))
+(assert (<= 0.0 a))
 (check-sat)
diff --git a/test/regress/cli/regress1/nl/proj-issue279.smt2 b/test/regress/cli/regress1/nl/proj-issue279.smt2
index 09ae1d378..e351011f9 100644
--- a/test/regress/cli/regress1/nl/proj-issue279.smt2
+++ b/test/regress/cli/regress1/nl/proj-issue279.smt2
@@ -1,5 +1,5 @@
 (set-logic ALL)
 (set-info :status sat)
 (declare-const s Real)
-(assert (or (or false (= 0.0 s)) (< (* s (+ 6 (* s 12))) (- 1))))
+(assert (or (or false (= 0.0 s)) (< (* s (+ 6.0 (* s 12.0))) (- 1.0))))
 (check-sat)
diff --git a/test/regress/cli/regress1/nl/proj-issue290.smt2 b/test/regress/cli/regress1/nl/proj-issue290.smt2
index b5a43b6ff..21b9823d0 100644
--- a/test/regress/cli/regress1/nl/proj-issue290.smt2
+++ b/test/regress/cli/regress1/nl/proj-issue290.smt2
@@ -2,5 +2,5 @@
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
-(assert (= 1 (* (/ 0 0) (/ 0 0) (/ 1 0))))
+(assert (= 1.0 (* (/ 0.0 0.0) (/ 0.0 0.0) (/ 1.0 0.0))))
 (check-sat)
diff --git a/test/regress/cli/regress1/nl/proj-issue291.smt2 b/test/regress/cli/regress1/nl/proj-issue291.smt2
index 2a43414c4..8fd4dce8f 100644
--- a/test/regress/cli/regress1/nl/proj-issue291.smt2
+++ b/test/regress/cli/regress1/nl/proj-issue291.smt2
@@ -2,5 +2,5 @@
 (set-info :status sat)
 (declare-const x1 Real)
 (declare-fun s () Real)
-(assert (and (> (* x1 s x1) 1) (exists ((x Bool)) (=> (not true) false))))
+(assert (and (> (* x1 s x1) 1.0) (exists ((x Bool)) (=> (not true) false))))
 (check-sat)
diff --git a/test/regress/cli/regress1/nl/proj-issue302.smt2 b/test/regress/cli/regress1/nl/proj-issue302.smt2
index 44939c12b..98b97ed0c 100644
--- a/test/regress/cli/regress1/nl/proj-issue302.smt2
+++ b/test/regress/cli/regress1/nl/proj-issue302.smt2
@@ -2,5 +2,5 @@
 (set-info :status sat)
 (declare-fun s () Real)
 (declare-fun k () Real)
-(assert (>= (* s k) 1))
+(assert (>= (* s k) 1.0))
 (check-sat)
diff --git a/test/regress/cli/regress1/nl/shifting.smt2 b/test/regress/cli/regress1/nl/shifting.smt2
index e460532ae..baf82d214 100644
--- a/test/regress/cli/regress1/nl/shifting.smt2
+++ b/test/regress/cli/regress1/nl/shifting.smt2
@@ -13,8 +13,8 @@
 
 (declare-fun z () Real)
 
-(assert (= z (* 2 pi s)))
+(assert (= z (* 2.0 pi (to_real s))))
 
-(assert (> z 60))
+(assert (> z 60.0))
 
 (check-sat)
diff --git a/test/regress/cli/regress1/nl/shifting2.smt2 b/test/regress/cli/regress1/nl/shifting2.smt2
index 9122701f6..dc40d8885 100644
--- a/test/regress/cli/regress1/nl/shifting2.smt2
+++ b/test/regress/cli/regress1/nl/shifting2.smt2
@@ -13,7 +13,7 @@
 
 (declare-fun z () Real)
 
-(assert (= z (+ y (* 2 pi s))))
+(assert (= z (+ y (* 2.0 pi (to_real s)))))
 
 (assert (and (< (- pi) z) (< z pi)))
 
diff --git a/test/regress/cli/regress1/quantifiers/issue3250-syg-inf-q.smt2 b/test/regress/cli/regress1/quantifiers/issue3250-syg-inf-q.smt2
index bb6a63490..e2a19e578 100644
--- a/test/regress/cli/regress1/quantifiers/issue3250-syg-inf-q.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue3250-syg-inf-q.smt2
@@ -5,8 +5,8 @@
     (and  
         (and 
             (exists ((?b Real)) (forall ((?c Real)) (exists ((?d Real)) 
-            (or  (and  (and  (and (and (< (+ (+ (+ 0 (* 68.0 ?c)) 0) (* 33.0 a)) 0.0) (<= 0 2.0)) 
-            (or (<= 0 (+  (*  (+ (* 55.0 ?d) 0) (* 49.0 ?b)) 0))))))))))
+            (or  (and  (and  (and (and (< (+ (+ (+ 0.0 (* 68.0 ?c)) 0.0) (* 33.0 a)) 0.0) (<= 0.0 2.0)) 
+            (or (<= 0.0 (+  (*  (+ (* 55.0 ?d) 0.0) (* 49.0 ?b)) 0.0))))))))))
         )
     )
 ) 
diff --git a/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 b/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2
index 18671b4d0..f64ea8e72 100644
--- a/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2
@@ -10,5 +10,5 @@
 (declare-fun b () Real)
 (declare-fun c () Real)
 (declare-fun e () Real)
-(assert (forall ((d Real)) (and (or (< (/ (* (- a) d) 0) c) (> b 0.0)) (= (= d 0) (= e 0)))))
+(assert (forall ((d Real)) (and (or (< (/ (* (- a) d) 0.0) c) (> b 0.0)) (= (= d 0.0) (= e 0.0)))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/issue4412-cegqi-type.smt2 b/test/regress/cli/regress1/quantifiers/issue4412-cegqi-type.smt2
index da070d8d6..3b1948756 100644
--- a/test/regress/cli/regress1/quantifiers/issue4412-cegqi-type.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue4412-cegqi-type.smt2
@@ -1,4 +1,4 @@
 (set-logic ALL)
 (set-info :status unsat)
-(assert (forall ((a Real)) (= (* (to_int (+ a 1)) (to_int a)) 1)))
+(assert (forall ((a Real)) (= (* (to_int (+ a 1.0)) (to_int a)) 1)))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/issue4685-wrewrite.smt2 b/test/regress/cli/regress1/quantifiers/issue4685-wrewrite.smt2
index 3fe54e2c6..bef3ac2c1 100644
--- a/test/regress/cli/regress1/quantifiers/issue4685-wrewrite.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue4685-wrewrite.smt2
@@ -2,5 +2,5 @@
 ; EXPECT: sat
 (set-logic NIRA)
 (set-info :status sat)
-(assert (forall ((a Int) (b Int)) (or (> a 0) (<= a (/ 0 (+ 0.5 b))))))
+(assert (forall ((a Int) (b Int)) (or (> a 0) (<= (to_real a) (/ 0.0 (+ 0.5 (to_real b)))))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/issue5288-vts-real-int.smt2 b/test/regress/cli/regress1/quantifiers/issue5288-vts-real-int.smt2
index b36b8cc94..d99cb51d0 100644
--- a/test/regress/cli/regress1/quantifiers/issue5288-vts-real-int.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue5288-vts-real-int.smt2
@@ -4,6 +4,6 @@
 (set-info :status unsat)
 (assert
  (forall ((a Int) (b Int))
- (or (< a (/ 3 b (- 2)))
+ (or (< (to_real a) (/ 3.0 (to_real b) (- 2.0)))
   (forall ((c Int)) (or (<= c b) (>= c a))))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/issue5378-witness.smt2 b/test/regress/cli/regress1/quantifiers/issue5378-witness.smt2
index b8628a432..74c52f756 100644
--- a/test/regress/cli/regress1/quantifiers/issue5378-witness.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue5378-witness.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --sygus-inst --strings-exp
 ; EXPECT: unsat
 (set-logic ALL)
-(assert (forall ((a Int) (b Int)) (or (> a (/ 0 b)) (exists ((c Int)) (< a c b)))))
+(assert (forall ((a Int) (b Int)) (or (> (to_real a) (/ 0.0 (to_real b))) (exists ((c Int)) (< a c b)))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/issue5735-2-subtypes.smt2 b/test/regress/cli/regress1/quantifiers/issue5735-2-subtypes.smt2
index 76a58bdb7..6b932a052 100644
--- a/test/regress/cli/regress1/quantifiers/issue5735-2-subtypes.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue5735-2-subtypes.smt2
@@ -1,4 +1,4 @@
 (set-logic ALL)
 (set-info :status unsat)
-(assert (forall ((a Real)) (exists ((b Int)) (= (exists ((c Int)) (<= a c (+ a 1))) (and (>= b (/ a (+ a 1))) (< 1 (+ a 1)))))))
+(assert (forall ((a Real)) (exists ((b Int)) (= (exists ((c Int)) (<= a (to_real c) (+ a 1.0))) (and (>= (to_real b) (/ a (+ a 1.0))) (< 1.0 (+ a 1.0)))))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/issue5735-subtypes.smt2 b/test/regress/cli/regress1/quantifiers/issue5735-subtypes.smt2
index 300819007..78eb57c95 100644
--- a/test/regress/cli/regress1/quantifiers/issue5735-subtypes.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue5735-subtypes.smt2
@@ -2,5 +2,5 @@
 (set-info :status unsat)
 (declare-fun a () Bool)
 (assert (forall ((b Int) (c Bool) (d Int))
-(or (= d (/ 1 (ite c 9 0))) (<= (ite a 1 b) (/ 1 (ite c 9 0))))))
+(or (= (to_real d) (/ 1.0 (ite c 9.0 0.0))) (<= (ite a 1.0 (to_real b)) (/ 1.0 (ite c 9.0 0.0))))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/issue6845-nl-lemma-tc.smt2 b/test/regress/cli/regress1/quantifiers/issue6845-nl-lemma-tc.smt2
index 087137653..fd5bd3fbd 100644
--- a/test/regress/cli/regress1/quantifiers/issue6845-nl-lemma-tc.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue6845-nl-lemma-tc.smt2
@@ -6,7 +6,7 @@
 (declare-fun i () Int)
 (declare-fun i1 () Int)
 (assert (< 1.0 (to_real i)))
-(assert (distinct 0 (/ 7 (to_real i))))
+(assert (distinct 0.0 (/ 7.0 (to_real i))))
 (push)
 (assert (or (exists ((q Int)) (= 0 (* i i1)))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/issue7537-cegqi-comp-types.smt2 b/test/regress/cli/regress1/quantifiers/issue7537-cegqi-comp-types.smt2
index bc9691ece..4c53ddf61 100644
--- a/test/regress/cli/regress1/quantifiers/issue7537-cegqi-comp-types.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue7537-cegqi-comp-types.smt2
@@ -2,5 +2,5 @@
 (set-info :status sat)
 (declare-fun r1 () Real)
 (declare-fun r5 () Real)
-(assert (forall ((q102 Int)) (or (= q102 (/ r1 r5)) (= (= 0.0 q102) (< 1.0 (/ r1 r5))))))
+(assert (forall ((q102 Int)) (or (= (to_real q102) (/ r1 r5)) (= (= 0 q102) (< 1.0 (/ r1 r5))))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/issue8517-exp-exp.smt2 b/test/regress/cli/regress1/quantifiers/issue8517-exp-exp.smt2
index a98c6e5c2..ad8aaedcf 100644
--- a/test/regress/cli/regress1/quantifiers/issue8517-exp-exp.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue8517-exp-exp.smt2
@@ -2,5 +2,5 @@
 (set-logic ALL)
 (declare-const x Bool)
 (declare-const x1 Bool)
-(assert (forall ((r Real)) (= x (and x1 (= r 2) (= 0.0 (exp (exp 1.0))) (= 3 (/ (- r) (- r)))))))
+(assert (forall ((r Real)) (= x (and x1 (= r 2.0) (= 0.0 (exp (exp 1.0))) (= 3.0 (/ (- r) (- r)))))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/issue8520-cegqi-nl-cov.smt2 b/test/regress/cli/regress1/quantifiers/issue8520-cegqi-nl-cov.smt2
index 561e03d77..62a78e7db 100644
--- a/test/regress/cli/regress1/quantifiers/issue8520-cegqi-nl-cov.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue8520-cegqi-nl-cov.smt2
@@ -3,5 +3,5 @@
 ; EXPECT: unknown
 (set-logic ALL)
 (declare-fun e () Real)
-(assert (forall ((x Real)) (distinct (* e e) (+ 1 (* x x (- 1))))))
+(assert (forall ((x Real)) (distinct (* e e) (+ 1.0 (* x x (- 1.0))))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/mix-coeff.smt2 b/test/regress/cli/regress1/quantifiers/mix-coeff.smt2
index 23ecba49e..c9d6a7b44 100644
--- a/test/regress/cli/regress1/quantifiers/mix-coeff.smt2
+++ b/test/regress/cli/regress1/quantifiers/mix-coeff.smt2
@@ -1,4 +1,4 @@
 (set-logic LIRA)
 (set-info :status unsat)
-(assert (forall ((x Int) (y Int) (a Real) (z Int)) (or (> x (+ a (* (/ 2 3) y) (* (/ 4 5) z))) (< x (+ 10 (* 3 a) (* (/ 2 5) y) (* (/ 4 7) z))))))
+(assert (forall ((x Int) (y Int) (a Real) (z Int)) (or (> (to_real x) (+ a (* (/ 2 3) (to_real y)) (* (/ 4 5) (to_real z)))) (< (to_real x) (+ 10.0 (* 3.0 a) (* (/ 2 5) (to_real y)) (* (/ 4 7) (to_real z)))))))
 (check-sat)
diff --git a/test/regress/cli/regress1/sygus/issue3200.smt2 b/test/regress/cli/regress1/sygus/issue3200.smt2
index 8eb144c61..f1e2f5472 100644
--- a/test/regress/cli/regress1/sygus/issue3200.smt2
+++ b/test/regress/cli/regress1/sygus/issue3200.smt2
@@ -2,6 +2,6 @@
 ; COMMAND-LINE: --sygus-inference
 (set-logic ALL)
 (declare-fun v () Real)
-(assert (= (* v v) 0))
+(assert (= (* v v) 0.0))
 (check-sat)
 (exit)
diff --git a/test/regress/cli/regress1/sygus/issue3205.smt2 b/test/regress/cli/regress1/sygus/issue3205.smt2
index b560491cd..7111e175b 100644
--- a/test/regress/cli/regress1/sygus/issue3205.smt2
+++ b/test/regress/cli/regress1/sygus/issue3205.smt2
@@ -2,6 +2,6 @@
 ; COMMAND-LINE: --sygus-inference
 (set-logic ALL)
 (declare-fun a () Real) 
-(assert (= (* a a) 1))
+(assert (= (* a a) 1.0))
 (check-sat)
 (exit)
diff --git a/test/regress/cli/regress1/sygus/issue3514.smt2 b/test/regress/cli/regress1/sygus/issue3514.smt2
index c5e39d93a..08f82ecd2 100644
--- a/test/regress/cli/regress1/sygus/issue3514.smt2
+++ b/test/regress/cli/regress1/sygus/issue3514.smt2
@@ -9,5 +9,5 @@
      (< (+ a c) 0.0)
      (or (distinct a 0.0) (= b 5.0))
      (distinct (+ b c) 1.0)
-     (< c 1))))))
+     (< c 1.0))))))
 (check-sat)
diff --git a/test/regress/cli/regress1/sygus/issue3633.smt2 b/test/regress/cli/regress1/sygus/issue3633.smt2
index 564a50cca..30c98d4cc 100644
--- a/test/regress/cli/regress1/sygus/issue3633.smt2
+++ b/test/regress/cli/regress1/sygus/issue3633.smt2
@@ -2,5 +2,5 @@
 ; COMMAND-LINE: --sygus-inference
 (set-logic ALL)
 (declare-fun a () Real)
-(assert (distinct a (sin 2)))
+(assert (distinct a (sin 2.0)))
 (check-sat)
diff --git a/test/regress/cli/regress1/sygus/issue3634.smt2 b/test/regress/cli/regress1/sygus/issue3634.smt2
index ad6910773..07db0c961 100644
--- a/test/regress/cli/regress1/sygus/issue3634.smt2
+++ b/test/regress/cli/regress1/sygus/issue3634.smt2
@@ -3,5 +3,5 @@
 (set-logic ALL)
 (declare-fun a () Int)
 (declare-fun b () Real)
-(assert (= (/ 1 (to_real a)) b))
+(assert (= (/ 1.0 (to_real a)) b))
 (check-sat)
diff --git a/test/regress/cli/regress1/sygus/issue3947-agg-miniscope.smt2 b/test/regress/cli/regress1/sygus/issue3947-agg-miniscope.smt2
index 3d4951f35..e1fb48e3e 100644
--- a/test/regress/cli/regress1/sygus/issue3947-agg-miniscope.smt2
+++ b/test/regress/cli/regress1/sygus/issue3947-agg-miniscope.smt2
@@ -5,5 +5,5 @@
 (set-option :sygus-inference true)
 (declare-fun a () Real)
 (declare-fun b () Real)
-(assert (forall ((c Real)) (or (< c a) (< 0 b))))
+(assert (forall ((c Real)) (or (< c a) (< 0.0 b))))
 (check-sat)
diff --git a/test/regress/cli/regress1/sygus/issue4009-qep.smt2 b/test/regress/cli/regress1/sygus/issue4009-qep.smt2
index 67007bac2..b27901a11 100644
--- a/test/regress/cli/regress1/sygus/issue4009-qep.smt2
+++ b/test/regress/cli/regress1/sygus/issue4009-qep.smt2
@@ -5,5 +5,5 @@
 (set-logic ALL)
 (declare-fun a () Real)
 (declare-fun b () Real)
-(assert (forall ((c Real)) (and (xor (> c a) (= b 0)) (distinct (+ a b) 0))))
+(assert (forall ((c Real)) (and (xor (> c a) (= b 0.0)) (distinct (+ a b) 0.0))))
 (check-sat)