[Consolidated] Assertion Violations with proof

[muchang]

Assertion violation at ../src/smt/smt_conflict_resolution.cpp Line: 1259

[883] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_conflict_resolution.cpp
Line: 1259
conflict.get_kind() != b_justification::AXIOM
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[884] % 
[884] % cat small.smt2
(set-option :proof true)
(set-option :smt.phase_selection 5)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c (Int) Bool)
(assert (= 0 (ite true (ite (c 0) 1 0) 0)))
(assert (= b (ite (= a 0) (+ b 1) b)))
(check-sat)
[885] % 

Commit: 4db41c0

[muchang]

Assertion violation at ../src/ast/ast.h Line: 717

[891] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.h
Line: 717
idx < m_num_args
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[892] % 
[892] % cat small.smt2
(set-option :smt.dack.eq true)
(set-option :smt.clause_proof true)
(set-option :proof true)
(declare-datatypes ((b!11 0) (e! 0) (j!7 0)) (((i(! e!))) (f (g(! e!))) ((l!5 (a!2 b!11) (k j!7)) m!6)))
(declare-fun h!12 () j!7)
(declare-fun c!3 (j!7) j!7)
(assert (forall ((d!9 j!7)) (= (! d!9) (ite ((_ is m!6) d!9) m!6 (ite ((_ is l!5) d!9) (l!5 (! (a!2 d!9)) (c!3 (! d!9))) h!12)))))
(check-sat)
[893] % 

Commit: 4db41c0

[muchang]

Assertion violation at ../src/smt/dyn_ack.cpp Line: 60

[906] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/smt/dyn_ack.cpp
Line: 60
m.is_eq(eq)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[907] % 
[907] % cat small.smt2
(set-option :smt.clause_proof true)
(set-option :smt.random_seed 2)
(set-option :proof true)
(declare-datatypes ((k 0)) (((h (a k)) (b))))
(declare-datatypes ((Lst 0)) (((cons (c k) (i Lst)) (nil))))
(declare-fun d (k k) k)
(declare-fun count (k Lst) k)
(assert (exists ((n k) (e k)) (distinct (d (h n) e) (h e))))
(assert (forall ((f k) (l k) (j Lst)) (= (count f (cons l j)) (ite (distinct f l) (h (count f j)) (count f j)))))
(assert (forall ((n k) (f k) (g Lst)) (distinct (d (h b) (count n g)) (count n (cons f g)))))
(check-sat)
[908] % 

Commit: 4db41c0