mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

n

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-02 10:51:33 -07:00
parent 6520f43f9d
commit 04876ba8b7
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/fixplex_def.h
View file

@ -205,8 +205,7 @@ namespace polysat {
if (in_bounds(x))
return l_true;
auto val = value(x);
numeral delta = value2delta(x, value(x));
numeral new_value = value(x) + delta;
numeral new_value = (lo(x) - val < val - hi(x)) ? lo(x) : hi(x) - 1;
numeral b;
var_t y = select_pivot_core(x, new_value, b);
@ -302,6 +301,7 @@ namespace polysat {
template<typename Ext>
typename fixplex<Ext>::numeral
fixplex<Ext>::value2delta(var_t v, numeral const& value) const {
SASSERT(!in_bounds(v));
if (lo(v) - value < value - hi(v))
return lo(v) - value;
else