From 161c83795fe697ecbb47c6849e478cc6dc169472 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 Jan 2019 08:34:55 -0800 Subject: [PATCH] remember inconsistent states when cloning Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 66655e2aa..f6a8698f4 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -120,6 +120,11 @@ namespace sat { m_qhead = 0; m_trail.reset(); m_scopes.reset(); + + if (src.inconsistent()) { + set_conflict(justification()); + return; + } // create new vars for (bool_var v = num_vars(); v < src.num_vars(); v++) {