Assertion violation at src/ast/ast.cpp:431

[wintered]

% z3-9be7bda bug.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 431
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 431
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
% cat bug.smt2
(set-option :smt.random_seed 1) 
(set-option :proof true) 
(set-option :trace true)    
(declare-fun a () Real) 
(declare-fun b () Real)   
(assert (not (=> (= a b) (< a (*  (+ (+ (div 2.0 b))))) (< 0 a))))  
(check-sat) 

OS: Ubuntu 18.04
Commit: 53b5ca3

[NikolajBjorner]

seems dup