Assertion violation: File: ../src/math/simplex/model_based_opt.cpp, Line: 200

[merlinsun]

Hi,
For this instance, z3 f014e30 debug build

$ cat small.smt2
(assert (forall ((v Real)) (distinct 1 (mod (to_int v) 3))))
(check-sat-using qsat)
$ z3 small.smt2
ASSERTION VIOLATION
File: ../src/math/simplex/model_based_opt.cpp
Line: 200
r.m_type != t_eq || r.m_value.is_zero()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
t
unknown

[merlinsun]

Another related instance with new core:

$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
ASSERTION VIOLATION
File: ../src/math/simplex/model_based_opt.cpp
Line: 200
r.m_type != t_eq || r.m_value.is_zero()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
t
unknown
$ cat delta.smt2
(declare-const x Int)
(assert (forall ((v Real)) (or (= v 0) (distinct 1 (mod x 3)))))
(check-sat)

[zhendongsu]

Another instance for the debug build in the default mode:

[578] % z3release small.smt2
unsat
[579] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/math/simplex/model_based_opt.cpp
Line: 200
r.m_type != t_eq || r.m_value.is_zero()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[580] % cat small.smt2
(assert (forall ((a Int)) (distinct (mod a 2) 1)))
(check-sat)