From bc8ddedc54e8492d5caed5a3fe7c1224bf4fdbfd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 14 Jun 2018 08:34:52 -0700
Subject: [PATCH] fix a few build regressions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_solver.cpp        | 2 --
 src/ast/arith_decl_plugin.cpp | 1 +
 src/qe/qe_solve_plugin.cpp    | 4 ++--
 src/smt/smt_setup.cpp         | 4 ++--
 4 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index ad5e7731d..951b9e51e 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -536,7 +536,6 @@ extern "C" {
         init_solver(c, s);
         expr_ref_vector _assumptions(m), _consequences(m), _variables(m);
         ast_ref_vector const& __assumptions = to_ast_vector_ref(assumptions);
-        unsigned sz = __assumptions.size();
         for (ast* e : __assumptions) {
             if (!is_expr(e)) {
                 _assumptions.finalize(); _consequences.finalize(); _variables.finalize();
@@ -546,7 +545,6 @@ extern "C" {
             _assumptions.push_back(to_expr(e));
         }
         ast_ref_vector const& __variables = to_ast_vector_ref(variables);
-        sz = __variables.size();
         for (ast* a : __variables) {
             if (!is_expr(a)) {
                 _assumptions.finalize(); _consequences.finalize(); _variables.finalize();
diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index fe5bc3af5..d2b17daa0 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -401,6 +401,7 @@ inline decl_kind arith_decl_plugin::fix_kind(decl_kind k, unsigned arity) {
 
 app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
     if (is_int && !val.is_int()) {
+        SASSERT(false);
         m_manager->raise_exception("invalid rational value passed as an integer");
     }
     if (val.is_unsigned()) {
diff --git a/src/qe/qe_solve_plugin.cpp b/src/qe/qe_solve_plugin.cpp
index 0a499d3b8..1f314848f 100644
--- a/src/qe/qe_solve_plugin.cpp
+++ b/src/qe/qe_solve_plugin.cpp
@@ -80,8 +80,8 @@ namespace qe {
                 bool sign = todo.back().first;
                 todo.pop_back();
                 if (a.is_add(e)) {
-                    for (expr* e : *to_app(e)) {
-                        todo.push_back(std::make_pair(sign, e));
+                    for (expr* arg : *to_app(e)) {
+                        todo.push_back(std::make_pair(sign, arg));
                     }
                 }
                 else if (a.is_sub(e)) {
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 97f5c433c..b90f08cd3 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -730,8 +730,8 @@ namespace smt {
     }
 
     void setup::setup_i_arith() {
-        m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
-        // m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));        
+        // m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
+        m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));        
     }
 
     void setup::setup_r_arith() {