From 2b18627fa1b1d884ee4be4a1c0aef88707fce8ed Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 7 Sep 2018 11:15:23 -0700
Subject: [PATCH] fix assertions (#83)

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp   | 6 +++++-
 src/util/lp/int_solver.h | 6 ++++++
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index a5c44b81a..07a7b0131 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3262,6 +3262,10 @@ public:
 
     void init_model(model_generator & mg) {
         init_variable_values();
+        DEBUG_CODE(            
+            for (auto const& kv : m_variable_values) {
+                SASSERT(!m_solver->var_is_int(kv.first) || kv.second.is_int() || m.canceled());
+            });
         m_factory = alloc(arith_factory, m);
         mg.register_factory(m_factory);
         TRACE("arith", display(tout););
@@ -3322,7 +3326,7 @@ public:
         else {
             rational r = get_value(v);
             TRACE("arith", tout << "v" << v << " := " << r << "\n";);
-            SASSERT(!a.is_int(o) || r.is_int());
+            SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.canceled()));
             if (a.is_int(o) && !r.is_int()) r = floor(r);
             return alloc(expr_wrapper_proc, m_factory->mk_value(r,  m.get_sort(o)));
         }
diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h
index 90f064a43..b51ae95d5 100644
--- a/src/util/lp/int_solver.h
+++ b/src/util/lp/int_solver.h
@@ -60,6 +60,12 @@ struct ineq {
 typedef vector<ineq> lemma;
 
 class int_solver {
+    struct validate_model {
+        int_solver& s;
+        lia_move& r;
+        validate_model(int_solver& s, lia_move& r): s(s), r(r) {}
+        ~validate_model();
+    };
 public:
     // fields
     lar_solver          *m_lar_solver;