From ef9230d8f8ae1a39efa6c4d2e45c9ce9b72fd754 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Nov 2016 06:56:36 -0800 Subject: [PATCH] detect quantifiers in model expressions to quiet down failing model validation Signed-off-by: Nikolaj Bjorner --- src/ast/macros/macro_util.cpp | 4 ++-- src/cmd_context/cmd_context.cpp | 3 +++ 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index e1f44e927..91bff5ab5 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -181,7 +181,7 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); if (is_macro_head(lhs, num_decls) && !is_forbidden(to_app(lhs)->get_decl()) && - !occurs(to_app(lhs)->get_decl(), rhs) && !has_quantifiers(rhs)) { + !occurs(to_app(lhs)->get_decl(), rhs)) { head = to_app(lhs); def = rhs; return true; @@ -213,7 +213,7 @@ bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & h expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); if (is_macro_head(rhs, num_decls) && !is_forbidden(to_app(rhs)->get_decl()) && - !occurs(to_app(rhs)->get_decl(), lhs) && !has_quantifiers(lhs)) { + !occurs(to_app(rhs)->get_decl(), lhs)) { head = to_app(rhs); def = lhs; return true; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 3cf00c154..eb7b3ff44 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1568,6 +1568,9 @@ void cmd_context::validate_model() { // If r contains as_array/store/map/const expressions, then we do not generate the error. // TODO: improve evaluator for model expressions. // Note that, if "a" evaluates to false, then the error will be generated. + if (has_quantifiers(r)) { + continue; + } try { for_each_expr(contains_array, r); }