diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 428577de7..3b9b81448 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2086,7 +2086,7 @@ namespace sat {
     }
 
     lbool ba_solver::eval(model const& m, constraint const& c) const {
-        lbool v1 = c.lit() == null_literal ? l_true : value(c.lit());
+        lbool v1 = c.lit() == null_literal ? l_true : value(m, c.lit());
         switch (c.tag()) {
         case card_t: return eval(v1, eval(m, c.to_card())); 
         case pb_t:   return eval(v1, eval(m, c.to_pb()));
@@ -2118,7 +2118,7 @@ namespace sat {
     lbool ba_solver::eval(model const& m, card const& c) const {
         unsigned trues = 0, undefs = 0;
         for (literal l : c) {
-            switch (l.sign() ? ~m[l.var()] : m[l.var()]) {
+            switch (value(m, l)) {
             case l_true: trues++; break;
             case l_undef: undefs++; break;
             default: break;
@@ -2132,7 +2132,7 @@ namespace sat {
     lbool ba_solver::eval(model const& m, pb const& p) const {
         unsigned trues = 0, undefs = 0;
         for (wliteral wl : p) {
-            switch (wl.second.sign() ? ~m[wl.second.var()] : m[wl.second.var()]) {
+            switch (value(m, wl.second)) {
             case l_true: trues += wl.first; break;
             case l_undef: undefs += wl.first; break;
             default: break;
@@ -2174,7 +2174,7 @@ namespace sat {
         bool odd = false;
         
         for (auto l : x) {
-            switch (l.sign() ? ~m[l.var()] : m[l.var()]) {
+            switch (value(m, l)) {
             case l_true: odd = !odd; break;
             case l_false: break;
             default: return l_undef;
@@ -2736,9 +2736,10 @@ namespace sat {
     }
 
     bool ba_solver::clausify(pb& p) {
+        return false;
         if (get_config().m_card_solver) 
             return false;
-
+        
         bool ok = !p.learned();
         bool is_def = p.lit() != null_literal;
         for (wliteral wl : p) {
@@ -4094,21 +4095,21 @@ namespace sat {
     bool ba_solver::check_model(model const& m) const {
         bool ok = true;
         for (constraint const* c : m_constraints) {
-            if (!check_model(m, *c)) ok = false;
+            switch (eval(m, *c)) {
+            case l_false: 
+                IF_VERBOSE(0, verbose_stream() << "failed checking " << c->id() << ": " << *c << "\n";);
+                ok = false;
+                break;
+            case l_true:
+                break;
+            case l_undef:
+                IF_VERBOSE(0, verbose_stream() << "undef " << c->id() << ": " << *c << "\n";);
+                break;
+            }
         }
         return ok;
     }
 
-    bool ba_solver::check_model(model const& m, constraint const& c) const {
-        if (eval(m, c) != l_true) {
-            IF_VERBOSE(0, verbose_stream() << "failed checking " << c.id() << ": " << c << "\n";);
-            return false;
-        }
-        else {
-            return true;
-        }
-    }
-
     
 };
 
diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h
index 8ed303469..6b6d10c38 100644
--- a/src/sat/ba_solver.h
+++ b/src/sat/ba_solver.h
@@ -387,6 +387,8 @@ namespace sat {
         // access solver
         inline lbool value(bool_var v) const { return value(literal(v, false)); }
         inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
+        inline lbool value(model const& m, literal l) const { return l.sign() ? ~m[l.var()] : m[l.var()]; }
+
         inline unsigned lvl(literal lit) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(lit); }
         inline unsigned lvl(bool_var v) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(v); }
         inline bool inconsistent() const { 
@@ -467,7 +469,6 @@ namespace sat {
         void copy_core(ba_solver* result, bool learned);
         void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints);
 
-        bool check_model(model const& m, constraint const& c) const;
     public:
         ba_solver();
         virtual ~ba_solver();
diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp
index a59deeafd..c820aa4f8 100644
--- a/src/sat/sat_big.cpp
+++ b/src/sat/sat_big.cpp
@@ -42,7 +42,7 @@ namespace sat {
                     m_roots[v.index()] = false;
                     edges.push_back(v);
                 }
-#if 1
+#if 0
                 if (w.is_ext_constraint() && 
                     s.m_ext && 
                     learned &&