From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 5 May 2022 16:52:26 +0000 (-0500)
Subject: Fix more issues with subtypes in regressions (#8727)
X-Git-Tag: cvc5-1.0.1~166
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b54ac5405c2aeb470812e19d6c4c30eb246f65b2;p=cvc5.git

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 09170bead..2a74fad4d 100644
--- 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 9fea58744..cdf8d5700 100644
--- 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 25dc80223..5e2c3a468 100644
--- 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 0d0a9eccc..5f908db6e 100644
--- 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 a27a5db73..af1cbf717 100644
--- 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 23e6fa17d..def20a825 100644
--- 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)