Fix more issues with subtypes in regressions (#8727)

In preparation for making type rule for equality strict.

diff --git a/test/regress/cli/regress0/nl/issue8691-3-msum-subtypes.smt2 b/test/regress/cli/regress0/nl/issue8691-3-msum-subtypes.smt2
index 09170bead7b148f74416cdbff9106931955d38fc..2a74fad4d9974691f134f03a2db1e606af940b71 100644 (file)
--- a/test/regress/cli/regress0/nl/issue8691-3-msum-subtypes.smt2
+++ b/test/regress/cli/regress0/nl/issue8691-3-msum-subtypes.smt2
@@ -1,5 +1,5 @@
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun a () Int)
-(assert (distinct 0 (/ a (+ 0.5 a))))
+(assert (distinct 0.0 (/ a (+ 0.5 a))))
 (check-sat)

diff --git a/test/regress/cli/regress0/nl/issue8692-idem-flatten.smt2 b/test/regress/cli/regress0/nl/issue8692-idem-flatten.smt2
index 9fea5874481df5f40bee65338fb431b30583245e..cdf8d5700ebaa35f19bca8cf09e31f7a8f658af1 100644 (file)
--- a/test/regress/cli/regress0/nl/issue8692-idem-flatten.smt2
+++ b/test/regress/cli/regress0/nl/issue8692-idem-flatten.smt2
@@ -2,5 +2,5 @@
 (set-info :status sat)
 (declare-fun a () Int)
 (declare-fun b () Int)
-(assert (= 0 (* b (/ a (- 1)))))
+(assert (= 0.0 (* b (/ a (- 1)))))
 (check-sat)

diff --git a/test/regress/cli/regress1/fmf/issue3626.smt2 b/test/regress/cli/regress1/fmf/issue3626.smt2
index 25dc80223156535656ed6a6dbe67989f0e0588be..5e2c3a46803790899272cabfb83e162ad538c0ea 100644 (file)
--- a/test/regress/cli/regress1/fmf/issue3626.smt2
+++ b/test/regress/cli/regress1/fmf/issue3626.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --fmf-bound --no-cegqi
 ; EXPECT: sat
 (set-logic ALL)
-(assert (forall ((a Int)) (or (distinct (/ 0 0) a) (= (/ 0 a) 0))))
+(assert (forall ((a Int)) (or (distinct (/ 0 0) (to_real a)) (= (/ 0 a) 0.0))))
 (check-sat)

diff --git a/test/regress/cli/regress1/fmf/sort-inf-int-real.smt2 b/test/regress/cli/regress1/fmf/sort-inf-int-real.smt2
index 0d0a9eccc2330712271ca5b7afbb36cc75442e5d..5f908db6e328a8b9b33c68f533457ff9c0d0d65b 100644 (file)
--- a/test/regress/cli/regress1/fmf/sort-inf-int-real.smt2
+++ b/test/regress/cli/regress1/fmf/sort-inf-int-real.smt2
@@ -8,8 +8,8 @@
 (assert (forall ((x Int)) (or (= (f x) (h (to_real x))) (= (f x) (to_int (g x))))))
 (assert (not (= (f 3) (h 3.0))))
 (assert (not (= (f 5) (to_int (g 5)))))
-(assert (= (f 4) (g 8)))
-(assert (= (h 5.0) 0.0))
+(assert (= (to_real (f 4)) (g 8)))
+(assert (= (to_real (h 5.0)) 0.0))
 ; Sort inference fails to infer that x can be uninterpreted in this example,
 ; however, fmf is able to reason that all instances are sat.
 (check-sat)

diff --git a/test/regress/cli/regress1/nl/issue7948-3-unsound-sin-region.smt2 b/test/regress/cli/regress1/nl/issue7948-3-unsound-sin-region.smt2
index a27a5db7316e5a14d510d13024d2582debc6c755..af1cbf717f263db3ce011048fa41c823c05138ec 100644 (file)
--- a/test/regress/cli/regress1/nl/issue7948-3-unsound-sin-region.smt2
+++ b/test/regress/cli/regress1/nl/issue7948-3-unsound-sin-region.smt2
@@ -3,5 +3,5 @@
 (set-logic ALL)
 (declare-fun a () Real)
 (declare-fun b () Real)
-(assert (and (= a 0) (= b (cos a))))
+(assert (and (= a 0.0) (= b (cos a))))
 (check-sat)

diff --git a/test/regress/cli/regress1/nl/issue8162-drop-pi-bound.smt2 b/test/regress/cli/regress1/nl/issue8162-drop-pi-bound.smt2
index 23e6fa17dd1536ce3b0d0a54e841d0a6d7b31b28..def20a8250f930008f31bc86462d8328df595c97 100644 (file)
--- a/test/regress/cli/regress1/nl/issue8162-drop-pi-bound.smt2
+++ b/test/regress/cli/regress1/nl/issue8162-drop-pi-bound.smt2
@@ -3,6 +3,6 @@
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun v () Real)
-(assert (xor (= 0 (/ v 0)) (distinct 1 (/ 0 0))))
-(assert (forall ((V Real)) (distinct 0 (sin 1.0))))
+(assert (xor (= 0.0 (/ v 0.0)) (distinct 1.0 (/ 0 0))))
+(assert (forall ((V Real)) (distinct 0.0 (sin 1.0))))
 (check-sat)