From 26d40865faddb888dfd72afc55b85777c34e2c1c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Sep 2018 23:54:48 -0700 Subject: [PATCH] add verbose output to capture cases for empty cube Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 097d3f0fa..5de64b496 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -311,7 +311,10 @@ public: expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) override { if (!is_internalized()) { lbool r = internalize_formulas(); - if (r != l_true) return expr_ref_vector(m); + if (r != l_true) { + IF_VERBOSE(0, verbose_stream() << "internalize produced " << r << "\n"); + return expr_ref_vector(m); + } } convert_internalized(); obj_hashtable _vs; @@ -329,6 +332,7 @@ public: return result; } if (result == l_true) { + IF_VERBOSE(1, verbose_stream() << "formulas are SAT\n"); return expr_ref_vector(m); } expr_ref_vector fmls(m); @@ -345,6 +349,7 @@ public: vs.push_back(x); } } + if (fmls.empty()) { IF_VERBOSE(0, verbose_stream() << "no literals were produced in cube\n"); } return fmls; }