diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 9648fdb0e..7c83580ac 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -702,6 +702,8 @@ namespace smt {
     }
 
     void theory_pb::unwatch_literal(literal lit, ineq* c) {
+        if (static_cast<unsigned>(lit.var()) >= m_var_infos.size())
+            return;
         ptr_vector<ineq>* ineqs = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
         if (ineqs) {
             remove(*ineqs, c);