Fix sort inference for quantified variables of interpreted types (#2393)

diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index c4c0a8b473fc1fd04d488620cfd1677d3ff96ec5..74f2e4803adbcca2a0af01465b2f87a4005aba77 100644 (file)
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -367,12 +367,21 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map<
       if( d_var_types.find( n )!=d_var_types.end() ){
         return getIdForType( n.getType() );
       }else{
+        //apply sort inference to quantified variables
         for( size_t i=0; i<n[0].getNumChildren(); i++ ){
-          //apply sort inference to quantified variables
-          d_var_types[n][n[0][i]] = d_sortCount;
-          d_sortCount++;
-
-          //type of the quantified variable must be the same
+          TypeNode nitn = n[0][i].getType();
+          if( !nitn.isSort() )
+          {
+            // If the variable is of an interpreted sort, we assume the
+            // the sort of the variable will stay the same sort.
+            d_var_types[n][n[0][i]] = getIdForType( nitn );
+          }
+          else
+          {
+            // If it is of an uninterpreted sort, infer subsorts.
+            d_var_types[n][n[0][i]] = d_sortCount;
+            d_sortCount++;
+          }
           var_bound[ n[0][i] ] = n;
         }
       }

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 17a302192e098a7cb2e0a9b2b98d3dc2a182da14..1c37669ded3073eff2d47e327c68050cbdf0b188 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -438,6 +438,7 @@ REG0_TESTS = \
        regress0/fmf/quant_real_univ.cvc \
        regress0/fmf/sat-logic.smt2 \
        regress0/fmf/sc_bad_model_1221.smt2 \
+       regress0/fmf/sort-infer-typed-082718.smt2 \
        regress0/fmf/syn002-si-real-int.smt2 \
        regress0/fmf/tail_rec.smt2 \
        regress0/fp/simple.smt2 \
@@ -1282,7 +1283,7 @@ REG1_TESTS = \
        regress1/quantifiers/cdt-0208-to.smt2 \
        regress1/quantifiers/const.cvc \
        regress1/quantifiers/constfunc.cvc \
-       regress1/quantifiers/dump-inst.smt2 \  
+       regress1/quantifiers/dump-inst.smt2 \
        regress1/quantifiers/dump-inst-i.smt2 \
        regress1/quantifiers/dump-inst-proof.smt2 \
        regress1/quantifiers/ext-ex-deq-trigger.smt2 \

diff --git a/test/regress/regress0/fmf/sort-infer-typed-082718.smt2 b/test/regress/regress0/fmf/sort-infer-typed-082718.smt2
new file mode 100644 (file)
index 0000000..6d026ff
--- /dev/null
+++ b/test/regress/regress0/fmf/sort-infer-typed-082718.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --sort-inference --finite-model-find --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic ALL)
+(assert (not (exists ((X Int)) (not (= X 12)) )))
+(check-sat)
+