From f5c4800eecbfcbc94ce0ce491670f96a9fd6ea3c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 17 Mar 2016 15:29:48 +0000 Subject: [PATCH] reduce-args: last fix for may_be_unique to support quantified variables in arbitrary exprs --- src/tactic/core/reduce_args_tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index cfb9a1eb8..ec7353044 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -19,6 +19,7 @@ Notes: #include"tactical.h" #include"cooperate.h" #include"ast_smt2_pp.h" +#include"has_free_vars.h" #include"map.h" #include"rewriter_def.h" #include"extension_model_converter.h" @@ -99,7 +100,7 @@ struct reduce_args_tactic::imp { } else { base = e; } - return !is_var(base); + return !has_free_vars(base); } static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) {