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 0281805fbaee8da127c64b387dad029203a72045..120aea616f904b65bf880b041bc318f1e4f611dc 100644 (file)
--- 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 8023ea0a42b6ed52c52d4a04c9a63b85623be48d..fa1408536058dc0e3478089a0b6eed6e2ae0d20f 100644 (file)
--- 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 777526117f5fc64a6912e3a3e00ad6fc9c25ee60..a72d2648d56379422f64d3d06f90c6025637e62d 100644 (file)
--- 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 74bdc88781ca6e5b96d5151e991de57f6555201f..8a62b70647c657346ee3cf8cfbf64bc6a9884035 100644 (file)
--- 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 99bedad3a062fa8a842a8f4cacc4c60480835436..f436ca0e8ea1a46db59be090b7779b1768e6ae83 100644 (file)
--- 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 0ce6dc89d1093fb836c0bbf326104af9948d9f87..60492ea090ae16a4bc8aec6676df274a3909332b 100644 (file)
--- 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 a15191115faa643846414e4ddfa340c1a5868bda..c204ca0dea794889cf5030e531b0ba8898b33451 100644 (file)
--- 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 b922bb7fa68dae5371a2302410b925ce9a588557..c07fc554110b377e6a6a0e8c1fc940f7518cebc9 100644 (file)
--- 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 1047674393b920584045c5d540bd4aea934e5ea8..478f198ab75130c0e718abcc835ef901659c01a6 100644 (file)
--- 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 cc828deb1b9d3acabf5f4440691af7682fdefffc..db3137692e6f9d1039173257f97ec2016a15c6fa 100644 (file)
--- 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 765bcdc2cf47b3e37cdd9f30e0f6415e329eea1e..27bfac37c4bece429060f080246d3930d7b6ffeb 100644 (file)
--- 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 e7566d49525fd275713754fa8ff0b525f39d1aa4..ef61be47475f7c671e4b26557ea252d8c1508b61 100644 (file)
--- 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 f8ed3dd3c92e9a968c935190dbffce59f29b5352..5663671795bc69e3264997b21e7257f85fcf730a 100644 (file)
--- 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 1e72650c222a860d818425a4387f51b8ff941067..626f9846913ec20ac90154ad5609aeecb8042faf 100644 (file)
--- 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 d1fbc73d285615002aee5e8e3b4a19f28f334672..33753375f770d0181208ee79ada40877726d9c0c 100644 (file)
--- 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 d66e6aec78b51441bbf66fef28bad6e9ba73f6a2..832b1c9b942563cf96f98bf9d7bf8a18e60c1c2e 100644 (file)
--- 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 c4bffc3daf035e1ac9f23084267faadf9e7422d5..01b9aa53c0ae1ea8681aef0a88e4e04fcb67b8f8 100644 (file)
--- 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 8951cc797c3a130afa1058f20fa47e22a90bf5e6..7834ed5814fd9b187424a98990c66a2b18a6d855 100644 (file)
--- 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 5650351cd06afddcb4af3474d43d60f5741adef9..e99f677b033afb9ecb8a4e32ae57d8fd959f4ac4 100644 (file)
--- 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 092e8513f107437405652697c37da2c78c8c41e8..a83e60c190dda4426bd5efa3b7b55b42054e91f9 100644 (file)
--- 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 730db4b239439f61265186e0ebdac6b79ac5af11..9acc326d064d718e6b867ca321012b753d382b9a 100644 (file)
--- 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 eff66c77dae579736c000770e835ab21c0462cdc..75dbf0ac3340604aa73bc1e7315f0f5dbc2f281a 100644 (file)
--- 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 1acdab13b339dbb6d5abf021edeb8a432bc5d7a4..20f0a619004311b57044cf21dbd83be2a8014e63 100644 (file)
--- 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 13088e5516f4f41de0099a74d211b041e2fd8705..c74d7ad6aeec333633e0f4e69b72adda93cc0b1e 100644 (file)
--- 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 0d71007ac51babc1c6e3c844c45d91ef6ab48cc8..abeb65ba401f2ce3be91c0feba27042fef95d000 100644 (file)
--- 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 40fa6154f82fa1c9cfc271b26df4b78495a11257..37ff9de18a733d8dd695175a4ab05cd00e1a5f2f 100644 (file)
--- 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 1be656f19b56f7c1ec99c33c94b0a113311b2a09..0b24adb7e2094a0d2f49326dfa1972c5fbd25375 100644 (file)
--- 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 9599b6e6baf80438ab71fd5fb1a1fae31381d42a..8f7f2e5356c85e761f3c8bd7557d6cc5a280ad41 100644 (file)
--- 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 92c4dabba0c33ddd0a49c24d0c46861e5d3dd763..ba760bf885a71fe092502cf8a731fd92b7e31ca7 100644 (file)
--- 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 c97a1207494c8cc67e85386e3d3febf8238dfe6a..b6a745917d72f257083e016895a908e447ddb5c5 100644 (file)
--- 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 1b2711597a408370d591196a42bbcdcb02e72590..e8a0dafd9d1cf8ecb0094a02dabcb5e192a173d0 100644 (file)
--- 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 f928a51e7a1352d2dc1f9781439e1ec88d0b641f..a41fb0cddd4cf3516d2f1263b4bb36e4ba636691 100644 (file)
--- 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 6cb631b6b16ecd76bf6871189891fd88c4684e16..09893f57e4fc75efcd8241131c2179df8829be4a 100644 (file)
--- 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 c1fd76ad59897618c05f687366ff5a05f78346c7..cc2966babc98982844edcdece21462bd01ab1e9b 100644 (file)
--- 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 fc7fbb180dd0e5dbf350d23fa0b2db85a0ced489..4ea5d91e13605822e44d28d53c960de72c0a45a8 100644 (file)
--- 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 432218e732a9f9ab5a8933c4c00e620d3efb8dc4..3cd026fdf1b7a1cf6b4f78dfe480ea04baabcbd8 100644 (file)
--- 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 52eeedae611ac01e6cc6d7abc5684320d4047b09..770402ad970559c5a4d7a7e20c306e903a7e81ef 100644 (file)
--- 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 9329f4c56835b0f17f4bcbe200a84b496eecb7d6..d123bf9c4751765ed7f180238f36e5a7921b5ea6 100644 (file)
--- 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 feda1174038e2cf65270358d3705d0ff8507dbf9..cb57097ce1df11ada682b3e69f65a8018fa613df 100644 (file)
--- 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 380a66aac17c20e3a5c4e14b755f5bc80d508039..7e1b53ca0b45251150d4a831cbcade4201eecc4d 100644 (file)
--- 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 3c37f2cbafac26446bf2f0280b5a360563960b61..be00967b4aca0722428bdd224577624cb03853bb 100644 (file)
--- 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 c3070ed06725582aef5a2d07406cf6bbe8e15901..a0a8f715e20b0db6ba42233f6a165f76e7edab83 100644 (file)
--- 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 d664647a5f2b0b337d01eb7582c6a1fbcef60b83..9329eea555630f49fdad63aad184f8f3a9c7d209 100644 (file)
--- 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 5bb5f1eeee593f0da0983dcfff220078b119eec0..286b5978d8d26e6f0a7b787314098c104b7aec54 100644 (file)
--- 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 4ed0aa17fa8bb3f9859fe0202b9cc77d46672300..a88f8c316fc50e74521d2b1ce98ff8050f65638b 100644 (file)
--- 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 a18dc82f987a9d7cc10c781a8326e8d69c06027e..ae1fccf6d37d9356519881c886ff5646588c8e2f 100644 (file)
--- 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 149b6a535a7cdd00c8df1aa81e862e476bce77fc..9c3ac01b92921af381afdceac8fc7c099353af10 100644 (file)
--- 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 545ea3e67066a39526c386066dacac28f2941de0..cd114e31c8b4222023bfa63d8c303a41d0e3b0fb 100644 (file)
--- 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 1e09f8439813972571d7c668b96b3924f7e1dc42..9054735c8dc2e63f378a07b2339c1a2a4607dc7e 100644 (file)
--- 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 24951890e3ea3c31d7ba9324a8881c0cb2e9db99..6b1d6724d1a61d6e905d1b88f63074472c0dd200 100644 (file)
--- 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 bf8a7bccec9818089026acf66f22cd3008af8c8b..9f5595c77c8723797896f238c1c1bda94dc84d3c 100644 (file)
--- 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 09ae1d3786b8ba7a9aa2fc162db5f1655487c12b..e351011f93014edee93449f7208da7479716b82f 100644 (file)
--- 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 b5a43b6ff37caeac3ee8965d86b59c16e84ea283..21b9823d07b37f8658371d6b3a87622efb05c5aa 100644 (file)
--- 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 2a43414c418beaeb8ce4ef86418ffc4da2626b6f..8fd4dce8f3931f839b2125f8aed4204549c629af 100644 (file)
--- 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 44939c12bcb24006298cd8b9e58979baa02166c7..98b97ed0cec444ffa05a6bedb369625b3249b113 100644 (file)
--- 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 e460532aeb392716fb903ed7d1facd1a047c35a5..baf82d214483ef89b752198dca039c99cf7cc581 100644 (file)
--- 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 9122701f62e1c59572b05517657fea6e35cb3905..dc40d8885fb8de6b6b1ce3ecd9b06ff28b0f9e95 100644 (file)
--- 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 bb6a63490128f88933046e47654d653a410bceb6..e2a19e57879c532c4fad40a22888ca6f6fb166d0 100644 (file)
--- 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 18671b4d03470d81c312087fb74a253ffe51119a..f64ea8e723b189f7c2c3fe2d316aa182ddf3f95e 100644 (file)
--- 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 da070d8d6a8f288d148257b2f4ba9ec5b5d141d0..3b1948756fa5b4577e243d503728f60cbd496a34 100644 (file)
--- 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 3fe54e2c6000aff0caae707a96537fb17d271bae..bef3ac2c1f44b326cdc8dc23fdeb3bc1944740da 100644 (file)
--- 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 b36b8cc9437c03406cbd966938ac127a6cedbbf1..d99cb51d0b8cbfb18c5bc588ffd09053764f18b6 100644 (file)
--- 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 b8628a43262c633eca7a36b9403116d8d03a93fc..74c52f756bfc12dfeb4ec07361546f9f360c2bfb 100644 (file)
--- 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 76a58bdb7a9ec10a53555f8df88473e573460dc5..6b932a05240f1952f184bd8408290853fb75d82d 100644 (file)
--- 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 3008190071c9b6aedfe0f44f35cdac6eb9e5e8af..78eb57c95bbeb013a19a1c4c93fc3e37d6fef5d9 100644 (file)
--- 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 0871376530517192afeef96c8b5d6b287ebed01a..fd5bd3fbddd1fe4c9b03bd423f23e6dff092aed7 100644 (file)
--- 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 bc9691ece6af1b09a976c65469db0cc053bdc2af..4c53ddf61f4c0a47af78a246b8e1481ffe6e36c2 100644 (file)
--- 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 a98c6e5c2c353ef9796ec61e0b070882e109796f..ad8aaedcf2b2d45e8011ae47fcff0463f4e92e88 100644 (file)
--- 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 561e03d772d5910690e0c7a6c81c227c6192fbe1..62a78e7dbd9ef20c1a7f7ff0cb43b678dbe78183 100644 (file)
--- 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 23ecba49e75355265135dc3d84eec63085a7d588..c9d6a7b44933db263b8406137f4ebc78d52b7842 100644 (file)
--- 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 8eb144c61d4c07cf9fe77497868046285d62dc24..f1e2f54720505841af9f8c45212f1071bd1b534b 100644 (file)
--- 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 b560491cd80d4bb87f4c13b44dbebec36a99f75c..7111e175b5fe3ab5c4a0af34661777969706696f 100644 (file)
--- 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 c5e39d93ad983b79180583790b351e8667aa954c..08f82ecd256c579012e7a2a7701f8e7329fb7a53 100644 (file)
--- 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 564a50cca12e5c7d0969b4e7ec3c4211f7906476..30c98d4cc1899b7fa3c3ac62313c9981d67adc66 100644 (file)
--- 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 ad691077356bf2509aa2c33ddc74e5b111aea27e..07db0c961d0187868e9f07f1ba777c744af970c0 100644 (file)
--- 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 3d4951f35581db69aa31ebf0c1924f1831613201..e1fb48e3e55f435e12675323dd2c721bbd3f18bb 100644 (file)
--- 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 67007bac221307ea2026feacee18a589f8c6458c..b27901a1142f5e85d78225bf29594eabed3e3b5d 100644 (file)
--- 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)