Closed
Description
Hi,
For this following instance, z3 3baaba5 debug build
$ cat small.smt2
(declare-fun b (Int) Int)
(declare-fun v () Int)
(assert (forall ((V Int)) (distinct false (exists ((a Int)) (> (+ a (b 0)) 1)))))
(assert (forall ((r Int)) (<= (+ v (* 3 r)) (/ 1 25))))
(assert (< (b 0) 0))
(check-sat)
$ z3 small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/gomory.cpp
Line: 322
is_int(v)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
Metadata
Metadata
Assignees
Labels
No labels