1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 10e57e794..f24e4fc66 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -266,10 +266,10 @@ Node TheoryModel::getModelValue(TNode n) const
   if (ita != d_approximations.end())
   {
     // If the value of n is approximate based on predicate P(n), we return
-    // choice z. P(z).
+    // witness z. P(z).
     Node v = nm->mkBoundVar(n.getType());
     Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
-    Node answer = nm->mkNode(CHOICE, bvl, ita->second.substitute(n, v));
+    Node answer = nm->mkNode(WITNESS, bvl, ita->second.substitute(n, v));
     d_modelCache[n] = answer;
     return answer;
   }