From 5ca8628e0d58bda1a61f8a6a4d607169f32a603a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Jul 2021 13:42:54 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_solver.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 781a94c85..a6e58c6d1 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -214,6 +214,14 @@ namespace euf { TRACE("euf", tout << "explain " << l << " <- " << r << " " << probing << "\n";); DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true);); +#if 0 + if (r.size() == 5 && r[0] == literal(401, true) && r[1] == literal(259, false) && r[2] == literal(250, false) && + r[3] == literal(631, false) && r[4] == literal(639, false)) { + TRACE("euf", s().display(tout);); + exit(0); + } +#endif + if (!probing) log_antecedents(l, r); }