diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 11 |
1 files 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; } } |