ASSERTION VIOLATION at ./src/ast/ast.cpp, Line: 2858

[zhendongsu]

Commit: a2bac11
OS: Ubuntu 18.04
Related: #6689

[552] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 2858
to_app(get_fact(p1))->get_arg(1) == to_app(get_fact(p2))->get_arg(0)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[553] % cat small.smt2
(set-option :proof true)
(assert (not (forall ((a Int)) false)))
(check-sat-using purify-arith)

[zhendongsu]

Another related instance:

[509] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 2858
to_app(get_fact(p1))->get_arg(1) == to_app(get_fact(p2))->get_arg(0)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[510] % cat small.smt2
(set-option :proof true)
(set-option :rewriter.eq2ineq true)
(declare-fun a () Int)
(declare-fun b (Int) Int)
(assert (< 0 (b a)))
(assert (= (forall ((c Int)) (not (= c 0))) false))
(check-sat)