From 2e441e38c9c3ba202a4c215224c2526100dd422b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 8 May 2023 12:24:20 -0700 Subject: [PATCH] fix #6713 fix #6714 Signed-off-by: Nikolaj Bjorner --- src/ast/array_decl_plugin.cpp | 4 ++-- src/ast/simplifiers/dependent_expr_state.cpp | 2 +- src/smt/theory_arith_nl.h | 1 + 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 7c2b357c2a7..6778bec7cb5 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -315,13 +315,13 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) { func_decl * array_decl_plugin::mk_array_ext(unsigned arity, sort * const * domain, unsigned i) { if (arity != 2 || domain[0] != domain[1]) { - UNREACHABLE(); + m_manager->raise_exception("incorrect arguments passed to array-ext"); return nullptr; } sort * s = domain[0]; unsigned num_parameters = s->get_num_parameters(); if (num_parameters == 0 || i >= num_parameters - 1) { - UNREACHABLE(); + m_manager->raise_exception("incorrect arguments passed to array-ext"); return nullptr; } sort * r = to_sort(s->get_parameter(i).get_ast()); diff --git a/src/ast/simplifiers/dependent_expr_state.cpp b/src/ast/simplifiers/dependent_expr_state.cpp index d784e6fe42e..7d00708ac2a 100644 --- a/src/ast/simplifiers/dependent_expr_state.cpp +++ b/src/ast/simplifiers/dependent_expr_state.cpp @@ -81,7 +81,7 @@ void dependent_expr_state::freeze_recfun() { ast_mark visited; for (func_decl* f : rec.get_rec_funs()) { auto& d = rec.get_def(f); - if (!d.is_macro()) + if (!d.is_macro() && d.get_rhs()) freeze_terms(d.get_rhs(), false, visited); } m_trail.push(value_trail(m_num_recfun)); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index d6d30cb33a5..f44516cad0f 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -892,6 +892,7 @@ bool theory_arith::propagate_linear_monomial(theory_var v) { } tout << "\n";); + return true; }