diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-05 11:13:39 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-05 11:13:39 -0500 |
commit | 1bd02cac69871158d71c74b23aa94c99cd69bead (patch) | |
tree | 7675faf1a4c21d40744f3a1dc067964eb1b6ada5 /src/theory/quantifiers/sygus/sygus_pbe.cpp | |
parent | 044fb6315119e0ad2f1ce57354f72d20ff4c6dc7 (diff) |
Update default options for sygus (#2586)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 889f4d9c9..8050e97f8 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -364,12 +364,12 @@ Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr) // are not passive return Node::null(); } - e = d_tds->getSynthFunForEnumerator(e); + Node ee = d_tds->getSynthFunForEnumerator(e); Assert(!e.isNull()); - std::map<Node, bool>::iterator itx = d_examples_invalid.find(e); + std::map<Node, bool>::iterator itx = d_examples_invalid.find(ee); if (itx == d_examples_invalid.end()) { - unsigned nex = d_examples[e].size(); - Node ret = d_pbe_trie[e][tn].addPbeExample(tn, e, bvr, this, 0, nex); + unsigned nex = d_examples[ee].size(); + Node ret = d_pbe_trie[e][tn].addPbeExample(tn, ee, bvr, this, 0, nex); Assert(ret.getType() == bvr.getType()); return ret; } |