projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 541e194) | patch
Fix BV Optimization Boundary Condition when lower bound = upper bound + 1 (#6452)
authorOuyancheng <1024842937@qq.com>
Wed, 28 Apr 2021 23:10:51 +0000 (16:10 -0700)
committerGitHub <noreply@github.com>
Wed, 28 Apr 2021 23:10:51 +0000 (23:10 +0000)
commit9e5a4a3e6aca1b25cf1af4a6392003cb5ecb8866
tree92ccc180c69150cd7276d5cedd41913e110fad2dtree
parent541e19463a0a5dc44dc97a494ca295aae296091ecommit | diff
Fix BV Optimization Boundary Condition when lower bound = upper bound + 1 (#6452)

If lb = ub + 1 then (lb+ub)/2 =pivot == lb since it's rounding to -infinity.
and lb <= x < pivot will always be UNSAT.
We need to handle this differently.
And this only happens in minimization.
src/omt/bitvector_optimizer.cpp diff | blob | history
test/unit/theory/theory_bv_opt_white.cpp diff | blob | history