From 8ae42b5ae120b268d7b29e1545d377a0f2f6c410 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 10:23:26 -0700 Subject: [PATCH] fix #4433 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_finder.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 6ba4868cb..5b6e4638a 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -2386,9 +2386,9 @@ namespace smt { expr * e = q->get_expr(); reset_cache(); if (!m.inc()) return; - SASSERT(m_ttodo.empty()); - SASSERT(m_ftodo.empty()); - + m_ttodo.reset(); + m_ftodo.reset(); + if (is_clause(m, e)) { process_clause(e); }