From b54ac5405c2aeb470812e19d6c4c30eb246f65b2 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 5 May 2022 11:52:26 -0500
Subject: [PATCH] Fix more issues with subtypes in regressions (#8727)

In preparation for making type rule for equality strict.
---
 test/regress/cli/regress0/nl/issue8691-3-msum-subtypes.smt2   | 2 +-
 test/regress/cli/regress0/nl/issue8692-idem-flatten.smt2      | 2 +-
 test/regress/cli/regress1/fmf/issue3626.smt2                  | 2 +-
 test/regress/cli/regress1/fmf/sort-inf-int-real.smt2          | 4 ++--
 .../cli/regress1/nl/issue7948-3-unsound-sin-region.smt2       | 2 +-
 test/regress/cli/regress1/nl/issue8162-drop-pi-bound.smt2     | 4 ++--
 6 files changed, 8 insertions(+), 8 deletions(-)

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)
-- 
2.30.2