From e173f47af5ab1c7245c11e0f8d0711cfba79c90a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 11 Sep 2019 17:59:05 -0500
Subject: [PATCH] Fix type assertion in getSynthSolutions (#3252)

---
 src/theory/quantifiers/sygus/synth_conjecture.cpp | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 89978e34b..fcfef1541 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -1165,14 +1165,21 @@ void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map)
     // convert to lambda
     TypeNode tn = d_embed_quant[0][i].getType();
     const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+    Node fvar = d_quant[0][i];
     Node bvl = Node::fromExpr(dt.getSygusVarList());
     if (!bvl.isNull())
     {
+      // since we don't have function subtyping, this assertion should only
+      // check the return type
+      Assert(fvar.getType().isFunction());
+      Assert(fvar.getType().getRangeType().isComparableTo(bsol.getType()));
       bsol = nm->mkNode(LAMBDA, bvl, bsol);
     }
+    else
+    {
+      Assert(fvar.getType().isComparableTo(bsol.getType()));
+    }
     // store in map
-    Node fvar = d_quant[0][i];
-    Assert(fvar.getType().isComparableTo(bsol.getType()));
     sol_map[fvar] = bsol;
   }
 }
-- 
2.30.2