mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix #1277 fix #1278

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-30 10:15:27 -07:00
parent 2229a2fc1b
commit 8ff8c6433b
2 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/cmd_context/cmd_context.cpp
View file

@ -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)");
}

2
src/smt/theory_arith_nl.h
View file

@ -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) {