Fix spurious warning in sort inference (#2331)

3 files changed, 17 insertions, 1 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index e43f6675d..9db34bca2 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -434,7 +434,6 @@ REG0_TESTS = \
 	regress0/fmf/quant_real_univ.cvc \
 	regress0/fmf/sat-logic.smt2 \
 	regress0/fmf/sc_bad_model_1221.smt2 \
-	regress0/fmf/sort-inf-int.smt2 \
 	regress0/fmf/syn002-si-real-int.smt2 \
 	regress0/fmf/tail_rec.smt2 \
 	regress0/fp/simple.smt2 \
@@ -1115,6 +1114,8 @@ REG1_TESTS = \
 	regress1/fmf/radu-quant-set.smt2 \
 	regress1/fmf/refcount24.cvc.smt2 \
 	regress1/fmf/sc-crash-052316.smt2 \
+	regress1/fmf/sort-inf-int.smt2 \
+	regress1/fmf/sort-inf-int-real.smt2 \
 	regress1/fmf/with-ind-104-core.smt2 \
 	regress1/gensys_brn001.smt2 \
 	regress1/ho/auth0068.smt2 \
diff --git a/test/regress/regress1/fmf/sort-inf-int-real.smt2 b/test/regress/regress1/fmf/sort-inf-int-real.smt2
new file mode 100644
index 000000000..9944ee55c
--- /dev/null
+++ b/test/regress/regress1/fmf/sort-inf-int-real.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --finite-model-find --sort-inference --no-check-models
+; EXPECT: sat
+(set-logic UFLIRA)
+(set-info :status sat)
+(declare-fun f (Int) Int)
+(declare-fun g (Int) Real)
+(declare-fun h (Real) Int)
+(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))
+; 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/regress0/fmf/sort-inf-int.smt2 b/test/regress/regress1/fmf/sort-inf-int.smt2
index e4a8978d4..e4a8978d4 100644
--- a/test/regress/regress0/fmf/sort-inf-int.smt2
+++ b/test/regress/regress1/fmf/sort-inf-int.smt2