diff options
Diffstat (limited to 'src/theory/quantifiers/sygus_inst.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus_inst.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index f6827d1c4..e59b788b6 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -309,7 +309,7 @@ bool SygusInst::sendEvalUnfoldLemmas(const std::vector<Node>& lemmas) for (const Node& lem : lemmas) { Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl; - added_lemma |= d_qim.addPendingLemma(lem); + added_lemma |= d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); } return added_lemma; } @@ -545,7 +545,7 @@ void SygusInst::addCeLemma(Node q) if (d_ce_lemma_added.find(q) != d_ce_lemma_added.end()) return; Node lem = d_ce_lemmas[q]; - d_qim.addPendingLemma(lem); + d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); d_ce_lemma_added.insert(q); Trace("sygus-inst") << "Add CE Lemma: " << lem << std::endl; } |