mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

switch on new viable

Browse source
This commit is contained in:
Jakob Rath 2023-12-07 14:36:37 +01:00
parent 6e12c26a79
commit 970a68e749
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1161,7 +1161,7 @@ namespace polysat {
find_t viable::find_viable(pvar v, rational& lo) {
rational hi;
switch (find_viable2(v, lo, hi)) {
switch (find_viable2_new(v, lo, hi)) {
case l_true:
if (hi < 0) {
// fallback solver, treat propagations as decisions for now