diff options
Diffstat (limited to 'src/theory/arith/nl_model.cpp')
| -rw-r--r-- | src/theory/arith/nl_model.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index abb2a7921..0d47c8874 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -1296,7 +1296,7 @@ void NlModel::getModelValueRepair( pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); Trace("nl-model") << v << " approximated as " << pred << std::endl; Node witness; - if (options::modelWitnessChoice()) + if (options::modelWitnessValue()) { // witness is the midpoint witness = nm->mkNode( @@ -1314,7 +1314,7 @@ void NlModel::getModelValueRepair( } } // Also record the exact values we used. An exact value can be seen as a - // special kind approximation of the form (choice x. x = exact_value). + // special kind approximation of the form (witness x. x = exact_value). // Notice that the above term gets rewritten such that the choice function // is eliminated. for (size_t i = 0, num = d_check_model_vars.size(); i < num; i++) |