From 8ff8c6433b9c377bae84c5c72084eefa3fbded3a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 30 Sep 2017 10:15:27 -0700
Subject: [PATCH] fix #1277 fix #1278
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/cmd_context/cmd_context.cpp | 6 ++++++
src/smt/theory_arith_nl.h | 2 +-
2 files changed, 7 insertions(+), 1 deletion(-)
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index b2a4fc47f..95c030687 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -870,6 +870,12 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
lhs = m().mk_app(f, binding.size(), binding.c_ptr());
eq = m().mk_eq(lhs, e);
if (!ids.empty()) {
+ if (is_var(e)) {
+ ptr_vector<sort> domain;
+ for (expr* b : binding) domain.push_back(m().get_sort(b));
+ insert_macro(f->get_name(), domain.size(), domain.c_ptr(), e);
+ return;
+ }
if (!is_app(e)) {
throw cmd_exception("Z3 only supports recursive definitions that are proper terms (not binders or variables)");
}
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index a04c34706..230b6de77 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -780,7 +780,7 @@ namespace smt {
of a non linear monomial that is not satisfied by the current assignment.
if v >= l, then create the case split v >= l+1
else v <= u, then create the case split v <= u-1
- else do nothing and return false.
+ else create the bound v = 0 and case split on it.
*/
template<typename Ext>
bool theory_arith<Ext>::branch_nl_int_var(theory_var v) {