From 1f9d6858f2d9cc21e6869ad743d18d07e82b30e7 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 17 Aug 2018 12:08:48 -0500
Subject: [PATCH]  Fix spurious warning in sort inference (#2331)

---
 src/theory/sort_inference.cpp                     |  8 +++++---
 test/regress/Makefile.tests                       |  3 ++-
 test/regress/regress1/fmf/sort-inf-int-real.smt2  | 15 +++++++++++++++
 .../{regress0 => regress1}/fmf/sort-inf-int.smt2  |  0
 4 files changed, 22 insertions(+), 4 deletions(-)
 create mode 100644 test/regress/regress1/fmf/sort-inf-int-real.smt2
 rename test/regress/{regress0 => regress1}/fmf/sort-inf-int.smt2 (100%)

diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index b6e8f7553..c4c0a8b47 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -710,11 +710,13 @@ Node SortInference::simplifyNode(
         }
       }
       children[0] = d_symbol_map[op];
-      //make sure all children have been taken care of
-      for( size_t i=0; i<n.getNumChildren(); i++ ){
+      // make sure all children have been given proper types
+      for (size_t i = 0, size = n.getNumChildren(); i < size; i++)
+      {
         TypeNode tn = children[i+1].getType();
         TypeNode tna = getTypeForId( d_op_arg_types[op][i] );
-        if( tn!=tna ){
+        if (!tn.isSubtypeOf(tna))
+        {
           Trace("sort-inference-warn") << "Sort inference created bad child: " << n << " " << n[i] << " " << tn << " " << tna << std::endl;
           Assert( false );
         }
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
similarity index 100%
rename from test/regress/regress0/fmf/sort-inf-int.smt2
rename to test/regress/regress1/fmf/sort-inf-int.smt2
-- 
2.30.2