diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 63c881b93..e6a233d3c 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -704,7 +704,6 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         if (!get_lengths(b, lens, pos)) {
             return BR_FAILED;
         }
-        unsigned rsz = lens.size();
         unsigned i = 0;
         for (; i < m_lhs.size(); ++i) {
             expr* lhs = m_lhs.get(i);
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 823d334b3..08edb1001 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -238,8 +238,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
             func_decl* g = nullptr;
             VERIFY(m_ar.is_as_array(f, g));
             expr* def = nullptr;
-            quantifier* q = nullptr;
-            proof* def_pr = nullptr;
             if (m_def_cache.find(g, def)) {
                 result = def;
                 return BR_DONE;