ASSERTION VIOLATION, File: src/math/lp/int_solver.cpp, Line: 141

Commit: https://github.com/Z3Prover/z3/commit/1be692002d1da07a6e2b1a29bf1a23f38d94c0f4 OS: Ubuntu 22.04

[509] % z3debug small.smt2
sat
ASSERTION VIOLATION
File: ../src/math/lp/int_solver.cpp
Line: 141
!lia.is_fixed(v)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[510] % cat small.smt2
(set-option :smt.arith.propagation_mode 2)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert (= (mod 0 (to_int b)) 0))
(check-sat (= c 0))
(assert (= d a b))
(check-sat (= a 2.5))

Z3Prover / z3

ASSERTION VIOLATION, File: src/math/lp/int_solver.cpp, Line: 141 #6860