mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix by anomaly detection, issue #118
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
parent
bb210d225a
commit
c09ac5422b
|
@ -4075,7 +4075,7 @@ namespace realclosure {
|
|||
|
||||
void refine_rational_interval(rational_value * v, unsigned prec) {
|
||||
mpbqi & i = interval(v);
|
||||
if (!i.lower_is_open() && !i.lower_is_open()) {
|
||||
if (!i.lower_is_open() && !i.upper_is_open()) {
|
||||
SASSERT(bqm().eq(i.lower(), i.upper()));
|
||||
return;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue