From 6450ee33c58a9dc5e86b7a7b852af46277ce16d5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Sep 2017 08:25:48 -0700 Subject: [PATCH] disregard model validation when source expression contains uninterpreted theory functions Signed-off-by: Nikolaj Bjorner --- 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 260d49174..3f34f3128 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1763,7 +1763,7 @@ void cmd_context::validate_model() { continue; } try { - for_each_expr(contains_underspecified, r); + for_each_expr(contains_underspecified, a); } catch (contains_underspecified_op_proc::found) { continue;