diff --git a/src/api/julia/z3jl.cpp b/src/api/julia/z3jl.cpp
index 8cb96abec..5b04d4a17 100644
--- a/src/api/julia/z3jl.cpp
+++ b/src/api/julia/z3jl.cpp
@@ -451,7 +451,9 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
         .method("add", static_cast<void (optimize::*)(expr const &)>(&optimize::add))
         .method("add", static_cast<optimize::handle (optimize::*)(expr const &, unsigned)>(&optimize::add))
         .method("add", static_cast<void (optimize::*)(expr const &, expr const &)>(&optimize::add))
-        .method("add", static_cast<optimize::handle (optimize::*)(expr const &, char const *)>(&optimize::add))
+        .method("add",      static_cast<optimize::handle (optimize::*)(expr const &, unsigned)>(&optimize::add_soft))
+        .method("add_soft", static_cast<optimize::handle (optimize::*)(expr const &, unsigned)>(&optimize::add_soft))
+        .method("add_soft", static_cast<optimize::handle (optimize::*)(expr const &, char const *)>(&optimize::add_soft))
         .MM(optimize, maximize)
         .MM(optimize, minimize)
         .MM(optimize, push)
@@ -713,4 +715,4 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
         .method("parse_string", static_cast<expr_vector (context::*)(char const*, sort_vector const&, func_decl_vector const&)>(&context::parse_string))
         .method("parse_file", static_cast<expr_vector (context::*)(char const*)>(&context::parse_file))
         .method("parse_file", static_cast<expr_vector (context::*)(char const*, sort_vector const&, func_decl_vector const&)>(&context::parse_file));
-}
\ No newline at end of file
+}
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 72a0e4ab2..645ae0a15 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -160,11 +160,20 @@ struct evaluator_cfg : public default_rewriter_cfg {
         family_id fid = f->get_family_id();
         bool _is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
         br_status st = BR_FAILED;
+#if 1
+        struct pp {
+            func_decl* f;
+            expr_ref& r;
+            pp(func_decl* f, expr_ref& r) :f(f), r(r) {}
+            ~pp() { TRACE("model_evaluator", tout << mk_pp(f, r.m()) << " " << r << "\n";); }
+        };
+        pp _pp(f, result);
+#endif
         if (num == 0 && (fid == null_family_id || _is_uninterp || m_ar.is_as_array(f))) {
             expr * val = m_model.get_const_interp(f);
             if (val != nullptr) {
                 result = val;
-                st = m_ar.is_as_array(val)? BR_REWRITE1 : BR_DONE;
+                st = m_ar.is_as_array(val) /* || m.is_eq(val)*/ ? BR_REWRITE1 : BR_DONE;
                 TRACE("model_evaluator", tout << result << "\n";);
                 return st;
             }
@@ -250,6 +259,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
             expr* def = nullptr;
             if (m_def_cache.find(g, def)) {
                 result = def;
+                TRACE("model_evaluator", tout << result << "\n";);
                 return BR_DONE;
             }
             func_interp * fi = m_model.get_func_interp(g);
@@ -282,17 +292,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 args.append(stores[i].size(), stores[i].c_ptr());
                 val = m_ar.mk_store(args);
             }
+            TRACE("model_evaluator", tout << val << "\n";);
         }
     }
 
     bool get_macro(func_decl * f, expr * & def, quantifier * & , proof * &) {
-
-#define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
-
         func_interp * fi = m_model.get_func_interp(f);
-
+        def = nullptr;
         if (fi != nullptr) {
-            TRACE_MACRO;
             if (fi->is_partial()) {
                 if (m_model_completion) {
                     sort * s   = f->get_range();
@@ -304,24 +311,22 @@ struct evaluator_cfg : public default_rewriter_cfg {
             }
             def = fi->get_interp();
             SASSERT(def != nullptr);
-            return true;
         }
-
-        if (m_model_completion &&
+        else if (m_model_completion &&
             (f->get_family_id() == null_family_id ||
-             m.get_plugin(f->get_family_id())->is_considered_uninterpreted(f)))
-        {
-            TRACE_MACRO;
+             m.get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) {
             sort * s   = f->get_range();
             expr * val = m_model.get_some_value(s);
             func_interp * new_fi = alloc(func_interp, m, f->get_arity());
             new_fi->set_else(val);
             m_model.register_decl(f, new_fi);
             def = val;
-            return true;
+            SASSERT(def != nullptr);
         }
 
-        return false;
+        CTRACE("model_evaluator", def != nullptr, tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ") " << mk_pp(def, m) << "\n";);
+
+        return def != nullptr;
     }
 
     br_status evaluate_partial_theory_func(func_decl * f,
@@ -560,7 +565,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
         func_decl* f = m_ar.get_as_array_func_decl(to_app(a));
         func_interp* g = m_model.get_func_interp(f);
-        if (!g) return false;
+        if (!g) {
+            TRACE("model_evaluator", tout << "no interpretation for " << mk_pp(f, m) << "\n";);
+            return false;
+        }
         else_case = g->get_else();
         if (!else_case) {
             TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m) << "\n";);
@@ -669,8 +677,8 @@ void model_evaluator::reset(model_core &model, params_ref const& p) {
 void model_evaluator::operator()(expr * t, expr_ref & result) {
     TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
     m_imp->operator()(t, result);
-    TRACE("model_evaluator", tout << result << "\n";);
     m_imp->expand_stores(result);
+    TRACE("model_evaluator", tout << result << "\n";);
 }
 
 expr_ref model_evaluator::operator()(expr * t) {