Fix spurious warning in sort inference (#2331)

2 files changed, 28 insertions, 0 deletions

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/regress1/fmf/sort-inf-int.smt2 b/test/regress/regress1/fmf/sort-inf-int.smt2
new file mode 100644
index 000000000..e4a8978d4
--- /dev/null
+++ b/test/regress/regress1/fmf/sort-inf-int.smt2
@@ -0,0 +1,13 @@
+; 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) Int)
+(declare-fun h (Int) Int)
+(assert (forall ((x Int)) (or (= (f x) (h x)) (= (f x) (g x)))))
+(assert (not (= (f 3) (h 3))))
+(assert (not (= (f 5) (g 5))))
+(assert (= (f 4) (g 8)))
+
+(check-sat)