Assertion failed in superposition.ml

[mcoulont]

Hello

Sorry to disturb you again.

I'm on master now and I try to run the following zf file:

# Integers

data nat := Zero | Succ nat.

val One : nat.

assert One = Succ Zero.


# Lists

data list a := nil | cons a (list a).

val length : pi a. list a -> nat.

assert length nil = Zero.

assert forall l x.
	length (cons x l) = Succ (length l).

val rankedTerm : pi a. (list a) -> nat -> a.

assert forall l x.
	rankedTerm (cons x l) Zero = x.

assert forall l x n.
	rankedTerm (cons x l) (Succ n) = rankedTerm l n.


# F2

val isInF2 : nat -> prop. 

rewrite forall x.
	isInF2 x <=> (x = Zero || x = One).

I get File "src/prover_calculi/superposition.ml", line 2211, characters 13-19: Assertion failed

It seems that it works when I remove either of:

• the definition of length
• the definition of rankedTerm
• the definition of isInF2

KR
Marc

[c-cube]

I can reproduce that, but I really don't have time to look more into it right now, sorry.

[abentkamp]

@petarvukmirovic has fixed this bug on the bool_calculi branch. So maybe you could try that branch instead? I guess it will still take a while until it gets merged into master.

[mcoulont]

It works with the branch you told. Thanks.