mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
value()
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d3d392da41
commit
4fb729a7d2
|
@ -141,7 +141,7 @@ namespace opt {
|
|||
if (soft.value == l_true) {
|
||||
continue;
|
||||
}
|
||||
SASSERT(soft.value() == l_undef);
|
||||
SASSERT(soft.value == l_undef);
|
||||
expr* a = soft.s;
|
||||
lbool is_sat = s().check_sat(1, &a);
|
||||
switch (is_sat) {
|
||||
|
@ -169,7 +169,7 @@ namespace opt {
|
|||
if (soft.value != l_undef) {
|
||||
continue;
|
||||
}
|
||||
SASSERT(soft.value() == l_undef);
|
||||
SASSERT(soft.value == l_undef);
|
||||
if (i + 1 == sz) {
|
||||
expr* a = soft.s;
|
||||
lbool is_sat = s().check_sat(1, &a);
|
||||
|
|
Loading…
Reference in a new issue