Hi,
For this formula:
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun g () Real)
(assert
(and
(forall ((e Real)) (or (= (* b d) 0.0) (and (< 0.0 (/ 2.0 e c)) (< (* e c) g))))
(forall ((f Real)) (< 0.0 (* a c)))))
(check-sat)
Z3 debug branch throws out an assertion violation:
ASSERTION VIOLATION
File: ../src/util/old_vector.h
Line: 370
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
OS: Ubuntu 18.04
Commit: 9f16fee
Hi,
For this formula:
Z3 debug branch throws out an assertion violation:
OS: Ubuntu 18.04
Commit: 9f16fee