From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 11 Sep 2019 22:59:05 +0000 (-0500)
Subject: Fix type assertion in getSynthSolutions (#3252)
X-Git-Tag: cvc5-1.0.0~3966
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e173f47af5ab1c7245c11e0f8d0711cfba79c90a;p=cvc5.git

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 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;
   }
 }