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

add assertion back for failing unit test, add comment about what is the bug

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-23 11:35:01 +01:00
parent 5e7ff769b4
commit 93410ccd81
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -92,7 +92,6 @@ namespace polysat {
// c alone (+ variables) is now enough to represent the conflict. // c alone (+ variables) is now enough to represent the conflict.
core.reset(); core.reset();
core.set(c); core.set(c);
std::cout << "set c\n";
return c->contains_var(v) ? l_undef : l_true; return c->contains_var(v) ? l_undef : l_true;
} }
return l_false; return l_false;