fix #4920

Z3Prover · Jan 9, 2021 · 223bffd · 223bffd
1 parent 1a71dfa
commit 223bffd
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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);