summaryrefslogtreecommitdiff
path: root/src/theory/arith/nonlinear_extension.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/nonlinear_extension.cpp')
-rw-r--r--src/theory/arith/nonlinear_extension.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index ff2ec412b..e8b1b3b93 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -583,7 +583,7 @@ unsigned NonlinearExtension::filterLemmas(std::vector<Node>& lemmas,
Trace("nl-ext-et-debug")
<< "Check entailment of " << ch_lemma << "..." << std::endl;
std::pair<bool, Node> et = d_containing.getValuation().entailmentCheck(
- THEORY_OF_TYPE_BASED, ch_lemma);
+ options::TheoryOfMode::THEORY_OF_TYPE_BASED, ch_lemma);
Trace("nl-ext-et-debug") << "entailment test result : " << et.first << " "
<< et.second << std::endl;
if (et.first)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback