diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 3de37129e..31c9771b1 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -2054,7 +2054,7 @@ public class Context implements AutoCloseable {
     public SeqExpr MkNth(SeqExpr s, Expr index)
     {
         checkContextMatch(s, index);
-        return (SeqExpr) Expr.create(this, Native.Z3_mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
+        return (SeqExpr) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
     }
 
 
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 248344c21..8f78a9106 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -166,7 +166,9 @@ namespace qe {
         expr_ref val(m);
         for (unsigned j = 0; j < m_preds[level - 1].size(); ++j) {
             app* p = m_preds[level - 1][j].get();            
-            eval(p, val);            
+            eval(p, val); 
+            if (!m.inc())
+                return;
             if (m.is_false(val)) {
                 m_asms.push_back(m.mk_not(p));
             }
@@ -179,6 +181,8 @@ namespace qe {
         
         for (unsigned i = level + 1; i < m_preds.size(); i += 2) {
             for (unsigned j = 0; j < m_preds[i].size(); ++j) {
+                if (!m.inc())
+                    return;
                 app* p = m_preds[i][j].get();
                 max_level lvl = m_elevel.find(p);
                 bool use =