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

revert for now

Browse source
This commit is contained in:
Jakob Rath 2024-04-12 14:35:12 +02:00
parent 183f96b481
commit 06e5595e87
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/polysat/viable.cpp
View file

@ -896,7 +896,7 @@ next:
if (ebw < abw) { if (ebw < abw) {
// 'e' is the last entry of a hole. // 'e' is the last entry of a hole.
// This case is handled in explain_hole_overlap. // This case is handled in explain_hole_overlap.
return; // return; // TODO: disabled for now
} }
if (ebw < bw || aw != bw) { if (ebw < bw || aw != bw) {
@ -1072,7 +1072,7 @@ next:
SASSERT(eew < bew); SASSERT(eew < bew);
SASSERT(eew < aew); SASSERT(eew < aew);
// return; return; // TODO: disabled for now
verbose_stream() << "explain_hole_overlap:\n"; verbose_stream() << "explain_hole_overlap:\n";
display_explain(verbose_stream() << " before ", before) << "\n"; display_explain(verbose_stream() << " before ", before) << "\n";