mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-17 08:42:15 +00:00
Code Activity

return on conflict (missing from earlier commit)

Browse source
This commit is contained in:
Jakob Rath 2023-03-05 22:50:00 +01:00
parent 4f96249570
commit f6213bdaa6
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/viable.cpp
View file

@ -143,6 +143,8 @@ namespace polysat {
try_viable: try_viable:
if (intersect(v, sc)) { if (intersect(v, sc)) {
if (s.is_conflict())
return true;
rational val; rational val;
switch (find_viable(v, val)) { switch (find_viable(v, val)) {
case find_t::singleton: case find_t::singleton: