mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-04-30 11:28:26 -07:00
parent aff02ca905 bd1b930d7a
commit d6e2e1f28f
2 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/sat/sat_solver.cpp
View file

@ -3389,6 +3389,9 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
literal lit = *it; literal lit = *it;
if (value(lit) != l_undef) { if (value(lit) != l_undef) {
++num_fixed; ++num_fixed;
if (value(lit) == l_true && lvl(lit) == 1) {
VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq));
}
continue; continue;
} }
push(); push();

4
src/test/cnf_backbones.cpp
View file

@ -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) { void tst_cnf_backbones(char ** argv, int argc, int& i) {
if (i + 1 < argc) { 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]); cnf_backbones(use_chunk, argv[i + 1]);
++i; ++i;
if (use_chunk) ++i;
} }
} }