fix #6713 fix #6714

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · May 8, 2023 · 2e441e3 · 2e441e3
1 parent 6c24a70
commit 2e441e3
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 3 deletions.
diff --git 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
@@ -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
@@ -892,6 +892,7 @@ bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
           }
           tout << "\n";);
 
+
     return true;
 }