mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fixed bug in unsat core generation

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-13 09:11:54 -07:00
parent 6145ccc077
commit bccf07be0b
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
lib/asserted_formulas.cpp
View file

@ -873,11 +873,18 @@ bool asserted_formulas::solve_core() {
} }
void asserted_formulas::solve() { void asserted_formulas::solve() {
// This method is buggy when unsatisfiable cores are enabled.
// It may eliminate answer literals.
// Since I will remove asserted_formulas.cpp in the future, I just disabled it.
// Note: asserted_formulas.cpp is based on the obsolete preprocessing stack.
// Users should the solve-eqs tactic if they want to eliminate variables.
#if 0
while (solve_core()) { while (solve_core()) {
IF_IVERBOSE(10, verbose_stream() << "reducing...\n";); IF_IVERBOSE(10, verbose_stream() << "reducing...\n";);
flush_cache(); // collect garbage flush_cache(); // collect garbage
reduce_asserted_formulas(); reduce_asserted_formulas();
} }
#endif
} }
void asserted_formulas::reduce_asserted_formulas() { void asserted_formulas::reduce_asserted_formulas() {