ASSERTION VIOLATION: File: ../src/sat/smt/pb_solver.cpp, Line: 1841

[zhendongsu]

Commit: 6e5ced0
OS: Ubuntu 18.04

[511] % z3release small.smt2
sat
[512] % z3debug small.smt2
-857 == [watch: 0, slack: 3]@(l_undef):  | 852@(l_undef) + 853@(l_undef) + -855@(l_undef) + 2 * -854@(l_undef) >= 2
ASSERTION VIOLATION
File: ../src/sat/smt/pb_solver.cpp
Line: 1841
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[513] % cat small.smt2
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(declare-const d Int)
(declare-const e Int)
(declare-fun f () Int)
(declare-fun u () Int)
(declare-fun g () Int)
(assert b)
(assert c)
(assert a)
(assert (<= 1 f 3))
(assert (<= 0 u 1))
(assert (<= 0 g 1))
(assert (> d 512))
(assert (> (* d e) 0))
(assert (distinct f (+ g u u)))
(check-sat)