diff --git a/src/ast/csp_decl_plugin.h b/src/ast/csp_decl_plugin.h
index f6f15d70a..7c10bbfe9 100644
--- a/src/ast/csp_decl_plugin.h
+++ b/src/ast/csp_decl_plugin.h
@@ -63,7 +63,7 @@ Revision History:
 
 
 --*/
-#pragma once;
+#pragma once
 #include "ast/ast.h"
 
 enum js_sort_kind {
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index e939072e1..dd690a6a9 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1060,9 +1060,9 @@ namespace sat {
     uint64_t ba_solver::get_coeff(literal lit) const {
         int64_t c1 = get_coeff(lit.var());
         SASSERT(c1 < 0 == lit.sign());
-        uint64_t c = static_cast<uint64_t>(std::abs(c1));
-        m_overflow |= c != c1;
-        return c;
+        int64_t c = std::abs(c1);
+        m_overflow |= (c != c1);
+        return static_cast<uint64_t>(c);
     }
 
     ba_solver::wliteral ba_solver::get_wliteral(bool_var v) {
@@ -1630,7 +1630,7 @@ namespace sat {
                 mark_visited(v);
                 if (s().is_marked(v)) {
                     int64_t c = get_coeff(v);
-                    if (c == 0 || (c < 0 == consequent.sign())) {
+                    if (c == 0 || ((c < 0) == consequent.sign())) {
                         s().reset_mark(v);
                         --m_num_marks;
                     }
@@ -3538,7 +3538,7 @@ namespace sat {
                 }
                 ++m_stats.m_num_big_strengthenings;
                 p.set_removed();
-                constraint* c = add_pb_ge(null_literal, wlits, b, p.learned());
+                add_pb_ge(null_literal, wlits, b, p.learned());
                 return;
             }
         }
diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp
index d0fce359f..3a2af72cf 100644
--- a/src/shell/dimacs_frontend.cpp
+++ b/src/shell/dimacs_frontend.cpp
@@ -178,21 +178,21 @@ unsigned read_dimacs(char const * file_name) {
             std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl;
             exit(ERR_OPEN_FILE);
         }
-        parse_dimacs(in, *g_solver);
+        parse_dimacs(in, solver);
     }
     else {
-        parse_dimacs(std::cin, *g_solver);
+        parse_dimacs(std::cin, solver);
     }
-    IF_VERBOSE(20, g_solver->display_status(verbose_stream()););
+    IF_VERBOSE(20, solver.display_status(verbose_stream()););
     
     lbool r;
     vector<sat::literal_vector> tracking_clauses;
-    sat::solver solver2( p, limit);
-    if (p.get_bool("dimacs.core", false)) {        
+    sat::solver solver2(p, limit);
+    if (p.get_bool("dimacs.core", false)) {
+        g_solver = &solver2;        
         sat::literal_vector assumptions;
         track_clauses(solver, solver2, assumptions, tracking_clauses);
-        g_solver = &solver2;        
-        r = solver2.check(assumptions.size(), assumptions.c_ptr());
+        r = g_solver->check(assumptions.size(), assumptions.c_ptr());
     }
     else {
         r = g_solver->check();
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 21af24b32..83ff79d3c 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4455,7 +4455,6 @@ namespace smt {
             }
         }
         recfun::util u(m);
-        recfun::decl::plugin& p = u.get_plugin();
         func_decl_ref_vector recfuns = u.get_rec_funs();
         for (func_decl* f : recfuns) {
             auto& def = u.get_def(f);
@@ -4464,7 +4463,6 @@ namespace smt {
             func_interp* fi = alloc(func_interp, m, f->get_arity());
             // reverse argument order so that variable 0 starts at the beginning.
             expr_ref_vector subst(m);
-            unsigned idx = 0;
             for (unsigned i = 0; i < f->get_arity(); ++i) {
                 subst.push_back(m.mk_var(i, f->get_domain(i)));
             }
diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp
index 880d75d24..847ea7f5e 100644
--- a/src/smt/theory_jobscheduler.cpp
+++ b/src/smt/theory_jobscheduler.cpp
@@ -130,7 +130,6 @@ namespace smt {
 
     void theory_jobscheduler::new_eq_eh(theory_var v1, theory_var v2) {
         enode* e1 = get_enode(v1);
-        enode* e2 = get_enode(v2);
         enode* root = e1->get_root();
         unsigned r;
         if (u.is_resource(root->get_owner(), r)) {
@@ -712,7 +711,7 @@ namespace smt {
 
             time_t start_lb = std::numeric_limits<time_t>::max();
             time_t runtime_lb = std::numeric_limits<time_t>::max();
-            time_t end_ub = 0, runtime_ub = 0;
+            time_t end_ub = 0; // , runtime_ub = 0;
             for (job_resource const& jr : ji.m_resources) {
                 unsigned r = jr.m_resource_id;
                 res_info const& ri = m_resources[r];
@@ -784,6 +783,7 @@ namespace smt {
     // resource(j) = r => start(j) <= end[idx]  || start[idx+1] <= start(j);
     void theory_jobscheduler::assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq) {
         job_resource const& jr = get_job_resource(j, r);
+        (void) jr;
         vector<res_available>& available = m_resources[r].m_available;        
         SASSERT(resource_available(jr, available[idx]));
         literal l2 = mk_ge(m_jobs[j].m_start, available[idx1].m_start);
@@ -795,6 +795,7 @@ namespace smt {
     void theory_jobscheduler::assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq) {
         vector<res_available>& available = m_resources[r].m_available;        
         job_resource const& jr = get_job_resource(j, r);
+        (void) jr;
         SASSERT(resource_available(jr, available[idx]));
         literal l2 = mk_le(m_jobs[j].m_end, available[idx].m_end);
         literal l3 = mk_ge(m_jobs[j].m_start, available[idx1].m_start);
diff --git a/src/smt/theory_jobscheduler.h b/src/smt/theory_jobscheduler.h
index 59c3b975d..3b9a42595 100644
--- a/src/smt/theory_jobscheduler.h
+++ b/src/smt/theory_jobscheduler.h
@@ -18,7 +18,7 @@ Author:
 Revision History:
 
 --*/
-#pragma once;
+#pragma once
 
 #include "util/uint_set.h"
 #include "ast/csp_decl_plugin.h"