Fix spurious warning in sort inference (#2331)

diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index b6e8f7553ecebe25ac0ef60bc3cef860ae8d1a87..c4c0a8b473fc1fd04d488620cfd1677d3ff96ec5 100644 (file)
--- 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 e43f6675d79844074cb4764a63cfb26a7c8316ac..9db34bca22236a1845364348d75225b24139a93a 100644 (file)
--- 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/regress0/fmf/sort-inf-int.smt2 b/test/regress/regress0/fmf/sort-inf-int.smt2
deleted file mode 100644 (file)
index e4a8978..0000000
--- a/test/regress/regress0/fmf/sort-inf-int.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-; 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)

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 (file)
index 0000000..9944ee5
--- /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 (file)
index 0000000..e4a8978
--- /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)