Debug branch: proof Assertion violation at ../src/ast/ast.cpp Line: 2910

[muchang]

Hi,
For this formula:

(set-option :proof true) 
(declare-sort a$) 
(declare-sort c$) 
(declare-sort d$) 
(declare-sort f$) 
(declare-sort e$)   
(declare-fun comp$b (f$) e$) 
(declare-fun m$g (e$ d$) f$) 
(declare-fun m$ac (f$ a$) c$) 
(declare-fun m$aw (d$ a$) a$)  
(assert (forall ((?h f$) (?i d$) (?j f$) (?k d$)) (= (= (m$g (comp$b ?h) ?i) (m$g (comp$b ?j) ?k)) 
(forall ((?l a$)) (= (m$ac ?h (m$aw ?i ?l)) (m$ac ?j (m$aw ?k ?l)))) false)))  
(check-sat)

Z3 debug branch throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 2910
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

OS: Ubuntu 18.04
Commit: f913f29

[NikolajBjorner]

not taking proof bugs in debug branch. They are largely orthogonal