From c482ede7ffaacc7d62de672c143af9783a9d8025 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Jan 2013 09:09:29 -0800
Subject: [PATCH] Fix bug introduced last week, and detected in nightly
 regression tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/cmd_context/cmd_context.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 043dc45e6..b511786bf 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1415,7 +1415,7 @@ void cmd_context::validate_model() {
     params_ref p;
     p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree.
     p.set_uint("sort_store", true); 
-    p.set_bool("model_completion", true); 
+    p.set_bool("completion", true); 
     model_evaluator evaluator(*(md.get()), p);
     contains_array_op_proc contains_array(m());
     {