From fd88b18c0db55eb63d0cd0454b19810a8abee789 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 22 Jan 2020 17:02:58 -0600
Subject: [PATCH] Fix subtyping for instantiations where internal
 representatives are chosen (#3641)

---
 src/theory/quantifiers/equality_query.cpp | 4 +++-
 src/theory/quantifiers/instantiate.cpp    | 9 ++++-----
 test/regress/CMakeLists.txt               | 1 +
 test/regress/regress1/fmf/issue3626.smt2  | 5 +++++
 4 files changed, 13 insertions(+), 6 deletions(-)
 create mode 100644 test/regress/regress1/fmf/issue3626.smt2

diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index f72a0d1b4..13e7b2eb7 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -167,7 +167,9 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
       if( d_rep_score.find( r_best )==d_rep_score.end() ){
         d_rep_score[ r_best ] = d_reset_count;
       }
-      Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl;
+      Trace("internal-rep-select")
+          << "...Choose " << r_best << " with score " << r_best_score
+          << " and type " << r_best.getType() << std::endl;
       Assert(r_best.getType().isSubtypeOf(v_tn));
       v_int_rep[r] = r_best;
       if( r_best!=a ){
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index c6427a4c4..aec648037 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -126,17 +126,16 @@ bool Instantiate::addInstantiation(
     {
       terms[i] = getTermForType(tn);
     }
+    // Ensure the type is correct, this for instance ensures that real terms
+    // are cast to integers for { x -> t } where x has type Int and t has
+    // type Real.
+    terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn);
     if (mkRep)
     {
       // pick the best possible representative for instantiation, based on past
       // use and simplicity of term
       terms[i] = d_qe->getInternalRepresentative(terms[i], q, i);
     }
-    else
-    {
-      // ensure the type is correct
-      terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn);
-    }
     Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
     if (terms[i].isNull())
     {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5020fe6fd..65d7f2b31 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1225,6 +1225,7 @@ set(regress_1_tests
   regress1/fmf/german73.smt2
   regress1/fmf/issue2034-preinit.smt2
   regress1/fmf/issue3587.smt2
+  regress1/fmf/issue3626.smt2
   regress1/fmf/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2
   regress1/fmf/ko-bound-set.cvc
diff --git a/test/regress/regress1/fmf/issue3626.smt2 b/test/regress/regress1/fmf/issue3626.smt2
new file mode 100644
index 000000000..9f27dee01
--- /dev/null
+++ b/test/regress/regress1/fmf/issue3626.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: sat
+(set-logic ALL)
+(assert (forall ((a Int)) (or (distinct (/ 0 0) a) (= (/ 0 a) 0))))
+(check-sat)
-- 
2.30.2