From 421a093844d9249f2735ff4b0b44f6d2b086d81d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 28 Aug 2018 10:39:48 -0500
Subject: [PATCH] Fix sort inference for quantified variables of interpreted
 types (#2393)

---
 src/theory/sort_inference.cpp                 | 19 ++++++++++++++-----
 test/regress/Makefile.tests                   |  3 ++-
 .../regress0/fmf/sort-infer-typed-082718.smt2 |  6 ++++++
 3 files changed, 22 insertions(+), 6 deletions(-)
 create mode 100644 test/regress/regress0/fmf/sort-infer-typed-082718.smt2

diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index c4c0a8b47..74f2e4803 100644
--- 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 17a302192..1c37669de 100644
--- 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
index 000000000..6d026ff5b
--- /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)
+
-- 
2.30.2