ASSERTION VIOLATION File: ../src/smt/theory_lra.cpp Line: 1541

[wintered]

$z3/build-2020-03-10-7bcd345/z3 bug0_PRETTY.smt2 
ASSERTION VIOLATION
File: ../src/smt/theory_lra.cpp
Line: 1541
can_get_ivalue(v)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
^C^C
$cat bug0_PRETTY.smt2 
(define-fun a () Int 10) 
(define-fun b () Int 0) 
(define-fun c () Int 1) 
(define-fun d () Int 5) 
(declare-fun s0 () Int)       
(define-fun e () Int 0) 
(define-fun f () Int (- s0 )) 
(define-fun u () Int f ) 
(define-fun g () Int u ) 
(define-fun h () Bool (<= g d)) 
(define-fun i () Int f ) 
(define-fun j () Int i) 
(define-fun k () Int (+ c j)) 
(define-fun l () Int (ite h k j)) 
(define-fun m () Int l) 
(define-fun n () Int (div m a)) 
(define-fun o () Bool (>= m b)) 
(define-fun p () Bool o ) 
(define-fun q () Int (ite p b c)) 
(define-fun r () Int (* n q)) 
(define-fun s () Bool (distinct e r)) 
(define-fun t () Bool s ) 
(assert t)
(check-sat)

OS: Ubuntu 18.04
Commit: 7bcd345

[NikolajBjorner]

Fixed by e32020b