From 2c208e1d1002c25593ad2e1a637fdfe96628fda3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Apr 2017 10:23:00 -0700 Subject: [PATCH 1/2] Sat update Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 739a591e7..cd13ac7a4 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3291,6 +3291,9 @@ namespace sat { literal lit = *it; if (value(lit) != l_undef) { ++num_fixed; + if (value(lit) == l_true && lvl(lit) == 1) { + VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq)); + } continue; } push(); From bd1b930d7a1735da6de575a4c57784f720690c8b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Apr 2017 11:00:03 -0700 Subject: [PATCH 2/2] swap argument order of chunk with file Signed-off-by: Nikolaj Bjorner --- src/test/cnf_backbones.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index 3387e1a8e..c34e109d3 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -271,9 +271,9 @@ static void cnf_backbones(bool use_chunk, char const* file_name) { void tst_cnf_backbones(char ** argv, int argc, int& i) { if (i + 1 < argc) { - bool use_chunk = (i + 2 < argc && argv[i + 2] == std::string("chunk")); + bool use_chunk = (i + 2 < argc && argv[i + 1] == std::string("chunk")); + if (use_chunk) ++i; cnf_backbones(use_chunk, argv[i + 1]); ++i; - if (use_chunk) ++i; } }