diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-11 17:59:05 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-11 17:59:05 -0500 |
commit | e173f47af5ab1c7245c11e0f8d0711cfba79c90a (patch) | |
tree | 5fb742a04db51e69dfef8da8a1d6176afef821f4 /src | |
parent | 81cd457d729f845f1b76d457359a0ae9963c0f88 (diff) |
Fix type assertion in getSynthSolutions (#3252)
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; } } |