diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-20 17:18:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-20 17:18:02 -0500 |
| commit | b967cc5c8d84023c1b821c59b7bca736ffda6bed (patch) | |
| tree | b1900e3817888a0ff321d70da4a31796db82b0ee /src/theory/quantifiers/sygus/synth_conjecture.cpp | |
| parent | 16c2fe5ec2ebb29da131aa590a4a0b79b1e94dc9 (diff) | |
Fixes for sygus inference on quantifier free problems (#3202)
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 6fdbfd0bc..aabc2f1f3 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -1160,7 +1160,7 @@ void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map) } // store in map Node fvar = d_quant[0][i]; - Assert(fvar.getType() == bsol.getType()); + Assert(fvar.getType().isComparableTo(bsol.getType())); sol_map[fvar] = bsol; } } |