Fix type assertion in getSynthSolutions (#3252)

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 89978e34bc8c6d251b9958aaee562e5baa1ad17b..fcfef15415526873128e599e25da80b72897758f 100644 (file)
--- 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;
   }
 }