diff options
Diffstat (limited to 'src/theory/quantifiers/fmf/full_model_check.cpp')
| -rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.cpp | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index c3fa664d9..c4f83191b 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -725,8 +725,11 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i } // just add the instance d_triedLemmas++; - if (instq->addInstantiation( - f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC, true)) + if (instq->addInstantiation(f, + inst, + InferenceId::QUANTIFIERS_INST_FMF_FMC, + Node::null(), + true)) { Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; @@ -875,8 +878,11 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm, if (ev!=d_true) { Trace("fmc-exh-debug") << ", add!"; //add as instantiation - if (ie->addInstantiation( - f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, true)) + if (ie->addInstantiation(f, + inst, + InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, + Node::null(), + true)) { Trace("fmc-exh-debug") << " ...success."; addedLemmas++; |