mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

Re-fixing a bug in compute_implicant_literals()

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-09 10:34:05 -07:00
parent 8445e2a7a2
commit 4a2eb909bf
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/muz/spacer/spacer_util.cpp
View file

@ -603,6 +603,14 @@ namespace {
void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula, void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula,
expr_ref_vector &res) { expr_ref_vector &res) {
// flatten the formula and remove all trivial literals
// TBD: not clear why there is a dependence on it (other than
// not handling of Boolean constants by implicant_picker), however,
// it was a source of a problem on a benchmark
flatten_and(formula);
if (formula.empty()) {return;}
implicant_picker ipick (mev); implicant_picker ipick (mev);
ipick (formula, res); ipick (formula, res);
} }