mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

Add warning to not trust the unsat cores yet

Browse source
This commit is contained in:
Jakob Rath 2023-01-25 12:30:27 +01:00
parent 4dc05447ad
commit f91bb12f0e
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/solver.cpp
View file

@ -1311,6 +1311,7 @@ namespace polysat {
} }
void solver::unsat_core(dependency_vector& deps) { void solver::unsat_core(dependency_vector& deps) {
verbose_stream() << "WARNING: unsat_core requested but dependency tracking in polysat is TODO\n";
deps.reset(); deps.reset();
LOG("conflict" << m_conflict); LOG("conflict" << m_conflict);
for (auto c : m_conflict) { for (auto c : m_conflict) {