Closed
Description
Hi,
For this instance, z3 e6385f8 debug build
$ cat small.smt2
(declare-const x Real)
(push)
(assert (forall ((v Real)) (< (div (* 13 v) 4 x (* v (- 6)) 0.0) 0)))
(check-sat)
$ z3 small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/gomory.cpp
Line: 191
!is_int(v) || c.is_int()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
Metadata
Metadata
Assignees
Labels
No labels