From 3fd5d0eaba7ba04d88aca6106de1360224221ec6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Jul 2015 08:34:54 -0700
Subject: [PATCH 1/4] handle variables and quantifiers, fixes issue #150

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/base/hnf.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp
index 58b626808..54bd727d6 100644
--- a/src/muz/base/hnf.cpp
+++ b/src/muz/base/hnf.cpp
@@ -112,6 +112,12 @@ public:
         expr* n1, *n2;
         while (is_forall(n)) n = to_quantifier(n)->get_expr();
         if (m.is_implies(n, n1, n2) && is_predicate(n2)) {
+            if (is_var(n1)) {
+                return true;
+            }
+            if (is_quantifier(n1)) {
+                return false;
+            }
             app* a1 = to_app(n1);
             if (m.is_and(a1)) {
                 for (unsigned i = 0; i < a1->get_num_args(); ++i) {

From 940fed16e1ea4684119eec1217e6e3e25190d957 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Jul 2015 09:11:52 -0700
Subject: [PATCH 2/4] enforce stringstream formatting to avoid default format
 routine. fixes issue #149

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/context_params.cpp |  4 ++-
 src/muz/fp/datalog_parser.cpp      | 31 +++++++++--------
 src/muz/rel/dl_instruction.cpp     | 20 ++++++-----
 src/util/gparams.cpp               | 55 ++++++++++++++++++++----------
 src/util/z3_exception.cpp          |  2 +-
 src/util/z3_exception.h            |  3 +-
 6 files changed, 71 insertions(+), 44 deletions(-)

diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp
index 4ba26aceb..8eee593d9 100644
--- a/src/cmd_context/context_params.cpp
+++ b/src/cmd_context/context_params.cpp
@@ -45,7 +45,9 @@ void context_params::set_bool(bool & opt, char const * param, char const * value
         opt = false;
     }
     else {
-        throw default_exception("invalid value '%s' for Boolean parameter '%s'", value, param);
+        std::stringstream strm;
+        strm << "invalid value '" << value << "' for Boolean parameter '" << param;
+        throw default_exception(strm.str());
     }
 }
 
diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp
index f1080676d..41c0f77af 100644
--- a/src/muz/fp/datalog_parser.cpp
+++ b/src/muz/fp/datalog_parser.cpp
@@ -665,7 +665,7 @@ protected:
 
     dtoken unexpected(dtoken tok, char const* msg) {
 #if 1
-        throw default_exception("%s at line %u '%s' found '%s'\n", msg, 
+        throw default_exception(default_exception::fmt(), "%s at line %u '%s' found '%s'\n", msg, 
             m_lexer->get_line(), m_lexer->get_token_data(), dtoken_strings[tok]);
 
         SASSERT(false);
@@ -958,7 +958,7 @@ protected:
                     m_vars.insert(data.bare_str(), v);
                 }
                 else if (s != m_manager.get_sort(v)) {
-                    throw default_exception("sort: %s expected, but got: %s\n",
+                    throw default_exception(default_exception::fmt(), "sort: %s expected, but got: %s\n",
                         s->get_name().bare_str(), m_manager.get_sort(v)->get_name().bare_str());
                 }
                 args.push_back(v);
@@ -1074,7 +1074,7 @@ protected:
 
     sort * register_finite_sort(symbol name, uint64 domain_size, context::sort_kind k) {
         if(m_sort_dict.contains(name.bare_str())) {
-            throw default_exception("sort %s already declared", name.bare_str());
+            throw default_exception(default_exception::fmt(), "sort %s already declared", name.bare_str());
         }
         sort * s = m_decl_util.mk_sort(name, domain_size);
         m_context.register_finite_sort(s, k);
@@ -1084,7 +1084,7 @@ protected:
 
     sort * register_int_sort(symbol name) {
         if(m_sort_dict.contains(name.bare_str())) {
-            throw default_exception("sort %s already declared", name.bare_str());
+            throw default_exception(default_exception::fmt(), "sort %s already declared", name.bare_str());
         }
         sort * s = m_arith.mk_int();
         m_sort_dict.insert(name.bare_str(), s);
@@ -1094,7 +1094,7 @@ protected:
     sort * get_sort(const char* str) {
         sort * res;
         if(!m_sort_dict.find(str, res)) {
-            throw default_exception("unknown sort \"%s\"", str);
+            throw default_exception(default_exception::fmt(), "unknown sort \"%s\"", str);
         }
         return res;
     }
@@ -1104,7 +1104,7 @@ protected:
         if(m_arith.is_int(s)) {
             uint64 val;
             if(!string_to_uint64(name.bare_str(), val)) {
-                throw default_exception("Invalid integer: \"&s\"", name.bare_str());
+                throw default_exception(default_exception::fmt(), "Invalid integer: \"%s\"", name.bare_str());
             }
             res = m_arith.mk_numeral(rational(val, rational::ui64()), s);
         }
@@ -1295,7 +1295,7 @@ private:
             if(num==0) {
                 const_name = symbol("<zero element>");
             } else if(!m_number_names.find(num, const_name)) {
-                throw default_exception("unknown symbol number %I64u on line %d in file %s", 
+                throw default_exception(default_exception::fmt(), "unknown symbol number %I64u on line %d in file %s", 
                     num, m_current_line, m_current_file.c_str());
             }
             res =  mk_table_const(const_name, s);
@@ -1334,12 +1334,13 @@ private:
             }
             uint64 num;
             if(!read_uint64(ptr, num)) {
-                throw default_exception("number expected on line %d in file %s", 
+                throw default_exception(default_exception::fmt(), "number expected on line %d in file %s", 
                     m_current_line, m_current_file.c_str());
             }
             if(*ptr!=' ' && *ptr!=0) {
-                throw default_exception("' ' expected to separate numbers on line %d in file %s, got '%s'", 
-                                m_current_line, m_current_file.c_str(), ptr);
+                throw default_exception(default_exception::fmt(), 
+                                        "' ' expected to separate numbers on line %d in file %s, got '%s'", 
+                                        m_current_line, m_current_file.c_str(), ptr);
             }
             args.push_back(num);
         } while(!last);
@@ -1359,7 +1360,7 @@ private:
 
         func_decl * pred = m_context.try_get_predicate_decl(predicate_name);
         if(!pred) {
-            throw default_exception("tuple file %s for undeclared predicate %s", 
+            throw default_exception(default_exception::fmt(), "tuple file %s for undeclared predicate %s", 
                 m_current_file.c_str(), predicate_name.bare_str());
         }
         unsigned pred_arity = pred->get_arity();
@@ -1381,7 +1382,7 @@ private:
                 continue;
             }
             if(args.size()!=pred_arity) {
-                throw default_exception("invalid number of arguments on line %d in file %s", 
+                throw default_exception(default_exception::fmt(), "invalid number of arguments on line %d in file %s", 
                     m_current_line, m_current_file.c_str());
             }
 
@@ -1450,10 +1451,12 @@ private:
 
         const char * ptr = full_line;
         if(!read_uint64(ptr, num)) {
-            throw default_exception("number expected at line %d in file %s", m_current_line, m_current_file.c_str());
+            throw default_exception(default_exception::fmt(), 
+                                    "number expected at line %d in file %s", m_current_line, m_current_file.c_str());
         }
         if(*ptr!=' ') {
-            throw default_exception("' ' expected after the number at line %d in file %s", m_current_line, m_current_file.c_str());
+            throw default_exception(default_exception::fmt(), 
+                                    "' ' expected after the number at line %d in file %s", m_current_line, m_current_file.c_str());
         }
         ptr++;
 
diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp
index f8145b922..fb7bb9281 100644
--- a/src/muz/rel/dl_instruction.cpp
+++ b/src/muz/rel/dl_instruction.cpp
@@ -385,8 +385,9 @@ namespace datalog {
             if (!find_fn(r1, r2, fn)) {
                 fn = r1.get_manager().mk_join_fn(r1, r2, m_cols1, m_cols2);
                 if (!fn) {
-                    throw default_exception("trying to perform unsupported join operation on relations of kinds %s and %s",
-                        r1.get_plugin().get_name().bare_str(), r2.get_plugin().get_name().bare_str());
+                    throw default_exception(default_exception::fmt(), 
+                                            "trying to perform unsupported join operation on relations of kinds %s and %s",
+                                            r1.get_plugin().get_name().bare_str(), r2.get_plugin().get_name().bare_str());
                 }
                 store_fn(r1, r2, fn);
             }
@@ -447,7 +448,7 @@ namespace datalog {
             if (!find_fn(r, fn)) {
                 fn = r.get_manager().mk_filter_equal_fn(r, m_value, m_col);
                 if (!fn) {
-                    throw default_exception(
+                    throw default_exception(default_exception::fmt(), 
                         "trying to perform unsupported filter_equal operation on a relation of kind %s",
                         r.get_plugin().get_name().bare_str());
                 }
@@ -496,7 +497,7 @@ namespace datalog {
             if (!find_fn(r, fn)) {
                 fn = r.get_manager().mk_filter_identical_fn(r, m_cols.size(), m_cols.c_ptr());
                 if (!fn) {
-                    throw default_exception(
+                    throw default_exception(default_exception::fmt(), 
                         "trying to perform unsupported filter_identical operation on a relation of kind %s",
                         r.get_plugin().get_name().bare_str());
                 }
@@ -542,7 +543,7 @@ namespace datalog {
             if (!find_fn(r, fn)) {
                 fn = r.get_manager().mk_filter_interpreted_fn(r, m_cond);
                 if (!fn) {
-                    throw default_exception(
+                    throw default_exception(default_exception::fmt(), 
                         "trying to perform unsupported filter_interpreted operation on a relation of kind %s",
                         r.get_plugin().get_name().bare_str());
                 }
@@ -598,7 +599,7 @@ namespace datalog {
             if (!find_fn(reg, fn)) {
                 fn = reg.get_manager().mk_filter_interpreted_and_project_fn(reg, m_cond, m_cols.size(), m_cols.c_ptr());
                 if (!fn) {
-                    throw default_exception(
+                    throw default_exception(default_exception::fmt(), 
                         "trying to perform unsupported filter_interpreted_and_project operation on a relation of kind %s",
                         reg.get_plugin().get_name().bare_str());
                 }
@@ -838,7 +839,8 @@ namespace datalog {
             if (!find_fn(r1, r2, fn)) {
                 fn = r1.get_manager().mk_join_project_fn(r1, r2, m_cols1, m_cols2, m_removed_cols);
                 if (!fn) {
-                    throw default_exception("trying to perform unsupported join-project operation on relations of kinds %s and %s",
+                    throw default_exception(default_exception::fmt(), 
+                                            "trying to perform unsupported join-project operation on relations of kinds %s and %s",
                         r1.get_plugin().get_name().bare_str(), r2.get_plugin().get_name().bare_str());
                 }
                 store_fn(r1, r2, fn);
@@ -905,7 +907,7 @@ namespace datalog {
 
             const relation_base & s = *ctx.reg(m_source_reg);
             if (!s.from_table()) {
-                throw default_exception("relation is not a table %s",
+                throw default_exception(default_exception::fmt(), "relation is not a table %s",
                     s.get_plugin().get_name().bare_str());
             }
             ++ctx.m_stats.m_min;
@@ -963,7 +965,7 @@ namespace datalog {
             if (!find_fn(r, fn)) {
                 fn = r.get_manager().mk_select_equal_and_project_fn(r, m_value, m_col);
                 if (!fn) {
-                    throw default_exception(
+                    throw default_exception(default_exception::fmt(), 
                         "trying to perform unsupported select_equal_and_project operation on a relation of kind %s",
                         r.get_plugin().get_name().bare_str());
                 }
diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp
index 69f596c5d..97f84af6a 100644
--- a/src/util/gparams.cpp
+++ b/src/util/gparams.cpp
@@ -205,12 +205,17 @@ public:
         if (mod_name == symbol::null) {
             char const * new_name = get_new_param_name(param_name);
             if (new_name) {
-                throw exception("the parameter '%s' was renamed to '%s', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:%s' for the full description of the parameter",
-                                param_name.bare_str(), new_name, new_name);
+                std::stringstream strm;
+                strm << "the parameter '" << param_name
+                     << "', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:" << new_name
+                     << "' for the full description of the parameter";
+                throw exception(strm.str());
             }
             else if (is_old_param_name(param_name)) {
-                throw exception("unknown parameter '%s', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list", 
-                                param_name.bare_str());
+                std::stringstream strm;
+                strm << "unknown parameter '" << param_name 
+                     << "', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list";
+                throw default_exception(strm.str());
             }
             else {
                 std::stringstream strm;
@@ -290,10 +295,12 @@ public:
                 ps.set_bool(param_name, false);
             }
             else {
-                if (mod_name == symbol::null)
-                    throw exception("invalid value '%s' for Boolean parameter '%s'", value, param_name.bare_str());
-                else
-                    throw exception("invalid value '%s' for Boolean parameter '%s' at module '%s'", value, param_name.bare_str(), mod_name.bare_str());
+                std::stringstream strm;
+                strm << "invalid value '" << value << "' for Boolean parameter '" << param_name << "'";                
+                if (mod_name == symbol::null) {
+                    strm << " at module '" << mod_name << "'";
+                }
+                throw default_exception(strm.str());
             }
         }
         else if (k == CPK_SYMBOL) {
@@ -312,10 +319,12 @@ public:
             ps.set_str(param_name, symbol(value).bare_str());
         }
         else {
-            if (mod_name == symbol::null)
-                throw exception("unsupported parameter type '%s'", param_name.bare_str());
-            else
-                throw exception("unsupported parameter type '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str());
+            std::stringstream strm;
+            strm << "unsupported parameter type '" << param_name << "'";            
+            if (mod_name == symbol::null) {
+                strm << " at module '" << mod_name << "'";            
+            }
+            throw exception(strm.str());
         }
     }
 
@@ -338,7 +347,9 @@ public:
                         set(*d, p, value, m);
                     }
                     else {
-                        throw exception("invalid parameter, unknown module '%s'", m.bare_str());
+                        std::stringstream strm;
+                        strm << "invalid parameter, unknown module '" << m << "'";
+                        throw exception(strm.str());
                     }
                 }
             }
@@ -396,7 +407,9 @@ public:
                             r = get_default(*d, p, m);
                         }
                         else {
-                            throw exception("unknown module '%s'", m.bare_str());
+                            std::stringstream strm;
+                            strm << "unknown module '" << m << "'";
+                            throw exception(strm.str());
                         }
                     }
                 }
@@ -488,8 +501,11 @@ public:
         {
             try {
                 param_descrs * d = 0;
-                if (!get_module_param_descrs().find(module_name, d))
-                    throw exception("unknown module '%s'", module_name.bare_str());
+                if (!get_module_param_descrs().find(module_name, d)) {
+                    std::stringstream strm;
+                    strm << "unknown module '" << module_name << "'";                    
+                    throw exception(strm.str());
+                }
                 out << "[module] " << module_name;
                 char const * descr = 0;
                 if (get_module_descrs().find(module_name, descr)) {
@@ -522,8 +538,11 @@ public:
                     d = &get_param_descrs();
                 }
                 else {
-                    if (!get_module_param_descrs().find(m, d))
-                        throw exception("unknown module '%s'", m.bare_str());
+                    if (!get_module_param_descrs().find(m, d)) {
+                        std::stringstream strm;
+                        strm << "unknown module '" << m << "'";                    
+                        throw exception(strm.str());
+                    }
                 }
                 if (!d->contains(p))
                     throw_unknown_parameter(p, *d, m);
diff --git a/src/util/z3_exception.cpp b/src/util/z3_exception.cpp
index 52d42d27a..ee225ba48 100644
--- a/src/util/z3_exception.cpp
+++ b/src/util/z3_exception.cpp
@@ -58,7 +58,7 @@ unsigned z3_error::error_code() const {
     return m_error_code; 
 }
 
-default_exception::default_exception(char const* msg, ...) {
+default_exception::default_exception(fmt, char const* msg, ...) {
     std::stringstream out;
     va_list args;
     va_start(args, msg);
diff --git a/src/util/z3_exception.h b/src/util/z3_exception.h
index b059b5491..d7311f806 100644
--- a/src/util/z3_exception.h
+++ b/src/util/z3_exception.h
@@ -40,8 +40,9 @@ public:
 class default_exception : public z3_exception {
     std::string m_msg;
 public:
+    struct fmt {};
     default_exception(std::string const& msg);
-    default_exception(char const* msg, ...);
+    default_exception(fmt, char const* msg, ...);
     virtual ~default_exception() {}
     virtual char const * msg() const;
 };

From e2adcc19ecc0f772db5adf05986b66a003cca255 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Jul 2015 22:52:44 -0700
Subject: [PATCH 3/4] fix unit test for default exception

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/test/ex.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/test/ex.cpp b/src/test/ex.cpp
index 276d21cab..e9243dd5b 100644
--- a/src/test/ex.cpp
+++ b/src/test/ex.cpp
@@ -54,7 +54,7 @@ static void tst1() {
 
 static void tst2() {
     try {
-        throw default_exception("Format %d %s", 12, "twelve");
+        throw default_exception(default_exception::fmt(), "Format %d %s", 12, "twelve");
     }
     catch (z3_exception& ex) {
         std::cerr << ex.msg() << "\n";

From d815cf9b7b658a5393d8cc96ae1b6af13adb67cb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 7 Jul 2015 16:01:48 -0700
Subject: [PATCH 4/4] fix bug in optimization where a variable is updated twice

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith_aux.h  | 50 ++++++++++++++++++++++++++-----------
 src/smt/theory_arith_core.h |  1 +
 src/smt/theory_arith_inv.h  |  1 +
 src/smt/theory_arith_nl.h   |  3 +++
 4 files changed, 40 insertions(+), 15 deletions(-)

diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 862d9487e..33830d1a5 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1321,8 +1321,10 @@ namespace smt {
         typename svector<col_entry>::iterator end = c.end_entries();
         init_gains(x_j, inc, min_gain, max_gain);
         has_shared |= ctx.is_shared(get_enode(x_j));
+        bool empty_column = true;
         for (; it != end; ++it) {
             if (it->is_dead()) continue;
+            empty_column = false;
             row const & r = m_rows[it->m_row_id];
             theory_var s  = r.get_base_var();
             numeral const & coeff_ij = r[it->m_row_idx].m_coeff;
@@ -1333,7 +1335,6 @@ namespace smt {
             }
             has_shared |= ctx.is_shared(get_enode(s));
         }
-        bool empty_column = (c.begin_entries() == end);
         TRACE("opt", 
               tout << (safe_gain(min_gain, max_gain)?"safe":"unsafe") << "\n";
               tout << "min gain: " << min_gain;
@@ -1373,7 +1374,7 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::normalize_gain(numeral const& divisor, inf_numeral & max_gain) const {
         SASSERT(divisor.is_int());
-        if (!divisor.is_minus_one() && !divisor.is_one() && !max_gain.is_minus_one()) {
+        if (!divisor.is_minus_one() && !max_gain.is_minus_one()) {
             max_gain = floor(max_gain/divisor)*divisor;
         }
     }
@@ -1401,7 +1402,8 @@ namespace smt {
         TRACE("opt",
               tout << "v" << x << " := " << get_value(x) << " "
               << "min gain: " << min_gain << " " 
-              << "max gain: " << max_gain << "\n";);              
+              << "max gain: " << max_gain << "\n";);           
+                
 
         SASSERT(max_gain.is_minus_one() || !max_gain.is_neg());
         SASSERT(min_gain.is_minus_one() || min_gain.is_one());
@@ -1423,6 +1425,8 @@ namespace smt {
         // a_ij < 0, !inc -> decrement x_i
         // a_ij denominator
 
+        SASSERT(!a_ij.is_zero());
+
         if (!safe_gain(min_gain, max_gain)) return false;
 
         inf_numeral max_inc = inf_numeral::minus_one();
@@ -1438,8 +1442,13 @@ namespace smt {
         if (is_int(x_i)) den_aij = denominator(a_ij);
         SASSERT(den_aij.is_pos() && den_aij.is_int());
 
-        if (is_int(x_i) && !den_aij.is_one() && min_gain.is_pos()) {
-            min_gain = inf_numeral(lcm(min_gain.get_rational(), den_aij));
+        if (is_int(x_i) && !den_aij.is_one()) {
+            if (min_gain.is_neg()) {
+                min_gain = inf_numeral(den_aij);
+            }
+            else {
+                min_gain = inf_numeral(lcm(min_gain.get_rational(), den_aij));
+            }
             normalize_gain(min_gain.get_rational(), max_gain);
         }
 
@@ -1467,11 +1476,12 @@ namespace smt {
               << "min gain: " << min_gain << " " 
               << "max gain: " << max_gain << " tighter: "
               << (is_tighter?"true":"false") << "\n";);
+
         SASSERT(max_gain.is_minus_one() || !max_gain.is_neg());
         SASSERT(min_gain.is_minus_one() || !min_gain.is_neg());
-        //SASSERT(!is_int(x_i) || min_gain.is_pos());
-        //SASSERT(!is_int(x_i) || min_gain.is_int());
-        //SASSERT(!is_int(x_i) || max_gain.is_int());
+        SASSERT(!is_int(x_i) || min_gain.is_pos());
+        SASSERT(!is_int(x_i) || min_gain.is_int());
+        SASSERT(!is_int(x_i) || max_gain.is_int());
         return is_tighter;
     }
 
@@ -1510,6 +1520,7 @@ namespace smt {
         context& ctx = get_context();
 
         SASSERT(!maintain_integrality || valid_assignment());
+        SASSERT(satisfy_bounds());
 
         numeral a_ij, curr_a_ij, coeff, curr_coeff;
         inf_numeral min_gain, max_gain, curr_min_gain, curr_max_gain;
@@ -1538,15 +1549,17 @@ namespace smt {
                     // variable cannot be used for max/min.
                     continue; 
                 }
-                if (!pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, 
-                                       curr_min_gain, curr_max_gain, 
-                                       has_shared, curr_x_i)) {
+                bool picked_var = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, 
+                                                    curr_min_gain, curr_max_gain, 
+                                                    has_shared, curr_x_i);
+
+
+                SASSERT(!picked_var || safe_gain(curr_min_gain, curr_max_gain));
+                
+                if (!picked_var) {
                     best_efforts++;
                 }
-                else {
-                    SASSERT(safe_gain(curr_min_gain, curr_max_gain));
-                }
-                if (curr_x_i == null_theory_var) {
+                else if (curr_x_i == null_theory_var) {
                     TRACE("opt", tout << "unbounded\n";);
                     // we can increase/decrease curr_x_j as much as we want.
                     x_i   = null_theory_var; // unbounded
@@ -1584,6 +1597,7 @@ namespace smt {
             if (x_j == null_theory_var) {
                 TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";);
                 SASSERT(!maintain_integrality || valid_assignment());
+                SASSERT(satisfy_bounds());
                 result = OPTIMIZED;
                 break; 
             }
@@ -1599,14 +1613,17 @@ namespace smt {
                     update_value(x_j, max_gain);
                     TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";);
                     SASSERT(!maintain_integrality || valid_assignment());
+                    SASSERT(satisfy_bounds());
                     continue;
                 }
                 if (!inc && lower(x_j)) {
                     SASSERT(!unbounded_gain(max_gain));
+                    SASSERT(max_gain.is_pos());
                     max_gain.neg();
                     update_value(x_j, max_gain);
                     TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";);
                     SASSERT(!maintain_integrality || valid_assignment());
+                    SASSERT(satisfy_bounds());
                     continue;
                 }
 #if 0
@@ -1642,6 +1659,7 @@ namespace smt {
                 }
                 update_value(x_j, max_gain);
                 SASSERT(!maintain_integrality || valid_assignment());
+                SASSERT(satisfy_bounds());
                 continue;
             }
             
@@ -1670,6 +1688,7 @@ namespace smt {
             add_tmp_row(r, coeff, r2);
             SASSERT(r.get_idx_of(x_j) == -1);
             SASSERT(!maintain_integrality || valid_assignment());
+            SASSERT(satisfy_bounds());
         }
         TRACE("opt", display(tout););
         return (best_efforts>0)?BEST_EFFORT:result;
@@ -1749,6 +1768,7 @@ namespace smt {
         expr* e = get_enode(v)->get_owner();
 
         SASSERT(!maintain_integrality || valid_assignment());
+        SASSERT(satisfy_bounds());
         SASSERT(!is_quasi_base(v));
         if ((max && at_upper(v)) || (!max && at_lower(v))) {
             TRACE("opt", tout << "At bound: " << mk_pp(e, get_manager()) << "...\n";);
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 65105e65b..7a1625ffc 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -2154,6 +2154,7 @@ namespace smt {
         CASSERT("arith", wf_rows());
         CASSERT("arith", wf_columns());
         CASSERT("arith", valid_row_assignment());
+        CASSERT("arith", satisfy_bounds());
         return true;
     }
 
diff --git a/src/smt/theory_arith_inv.h b/src/smt/theory_arith_inv.h
index 9c56ea367..a23eb932d 100644
--- a/src/smt/theory_arith_inv.h
+++ b/src/smt/theory_arith_inv.h
@@ -196,6 +196,7 @@ namespace smt {
             CTRACE("bound_bug", below_lower(v) || above_upper(v), display_var(tout, v); display(tout););
             SASSERT(!below_lower(v));
             SASSERT(!above_upper(v));
+            if (below_lower(v) || above_upper(v)) return false;
         }
         return true;
     }
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index c2322fce2..56d2da1bf 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -2238,6 +2238,9 @@ namespace smt {
                 m_nl_gb_exhausted = true;
                 warn              = true;
             }
+            if (get_context().get_cancel_flag()) {
+                return GB_FAIL;
+            }
             TRACE("non_linear_gb", tout << "after:\n"; gb.display(tout););
             // Scan the grobner basis eqs, and look for inconsistencies.
             eqs.reset();