search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.42k stars 1.47k forks source link

Non-deterministic assertion violation on QF_NRA formula at nlsat_interval_set.cpp:99 #4335

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following instance 99.txt

(set-logic QF_NRA)
(set-option :model true)
(set-option :ackermannization.inc_sat_backend true)
(set-option :model.completion false)
(set-option :nlsat.shuffle_vars true)
(set-option :smt.phase_selection 2)
(set-option :smt.arith.solver 2)

z3 commie ce07138 throws an assertion violation

seq 20 | xargs -Iz /home/peisen/test/tofuzz/z3-debug/build/z3 timeout=10000 yy.smt2

unknown

ASSERTION VIOLATION
File: ../src/nlsat/nlsat_interval_set.cpp
Line: 99
curr.m_upper_open || next.m_lower_open

ASSERTION VIOLATION
File: ../src/nlsat/nlsat_interval_set.cpp
Line: 99
curr.m_upper_open || next.m_lower_open

unknown

...
NikolajBjorner commented 4 years ago

it is something related to cancellation and therefore more likely to be beningn. I can't repro it easily. It should be possible to repro more reliably using rlimit instead of timeout.