From e14bca2ebf0f852ee302c2f10a87ca9993e85b80 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Apr 2020 11:59:11 -0700 Subject: [PATCH] more graceful behavior of seq.validate #3885 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 42576f245..6e26e93f3 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -4585,10 +4585,6 @@ expr_ref theory_seq::elim_skolem(expr* e) { todo.pop_back(); continue; } - else if (m_util.is_skolem(a)) { - IF_VERBOSE(0, verbose_stream() << "unhandled skolem " << mk_pp(a, m) << "\n"); - return expr_ref(m.mk_false(), m); - } args.reset(); for (expr* arg : *to_app(a)) { @@ -4599,12 +4595,19 @@ expr_ref theory_seq::elim_skolem(expr* e) { todo.push_back(arg); } } - if (args.size() == to_app(a)->get_num_args()) { - todo.pop_back(); - result = m.mk_app(to_app(a)->get_decl(), args.size(), args.c_ptr()); - trail.push_back(result); - cache.insert(a, result); - } + if (args.size() < to_app(a)->get_num_args()) { + continue; + } + + if (m_util.is_skolem(a)) { + IF_VERBOSE(0, verbose_stream() << "unhandled skolem " << mk_pp(a, m) << "\n"); + return expr_ref(m.mk_false(), m); + } + + todo.pop_back(); + result = m.mk_app(to_app(a)->get_decl(), args.size(), args.c_ptr()); + trail.push_back(result); + cache.insert(a, result); } return expr_ref(cache[e], m); } @@ -4672,7 +4675,7 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons k.assert_expr(f); } lbool r = k.check(); - if (r != l_false) { + if (r != l_false && !m.limit().get_cancel_flag()) { model_ref mdl; k.get_model(mdl); IF_VERBOSE(0,