[nix-shell:/tmp/l/git/github/other/leon]$ ./leon --solvers=isabelle testcases/verification/Addresses.scala
./leon --solvers=isabelle testcases/verification/Addresses.scala
[Warning ] warning: there were two feature warnings; re-run with -feature for details
[ Info ] Preparing Isabelle setup (this might take a while) ...
[ Info ] Building session ...
[ Info ] Starting <Isabelle2016> instance ...
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Match uses unsupported features; translating to if-then-else
[Internal] Prover error in operation functions: ERROR "Type unification failed: Clash of types \"<markup>\" and \"<markup>\"\n\nType error in application: incompatible operand type\n\n<markup>\n<markup>\n\n<markup>"
[Internal] Offending input: List((collectA'37,List((x'35,Type(Int.int,List())), (l'36,Type(Leon_Runtime.List'2,List()))),(App(App(App(Const(HOL.If,Type(dummy,List())),App(Const(Leon_Runtime.List'2.dNil'8,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),App(App(Const(Product_Type.Pair,Type(dummy,List())),Const(Groups.zero_class.zero,Type(Int.int,List()))),App(App(Const(Product_Type.Pair,Type(dummy,List())),Const(Groups.zero_class.zero,Type(Int.int,List()))),Const(Leon_Runtime.List'2.cNil'8,Type(dummy,List()))))),App(App(App(Const(HOL.If,Type(dummy,List())),App(App(Const(HOL.conj,Type(dummy,List())),App(Const(Leon_Runtime.List'2.dCons'3,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),App(App(Const(HOL.eq,Type(dummy,List())),App(Const(Leon_Runtime.List'2.sa'4,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),Free(x'35,Type(Int.int,List()))))),App(App(Const(HOL.Let,Type(dummy,List())),App(App(Const(Product_Type.Pair,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),App(App(Free(collectA'37,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Leon_Runtime.List'2,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))))),Free(x'35,Type(Int.int,List()))),App(Const(Leon_Runtime.List'2.stail'7,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))))),App(App(Const(Product_Type.Pair,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),App(App(Free(collectA'37,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Leon_Runtime.List'2,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))))),Free(x'35,Type(Int.int,List()))),App(Const(Leon_Runtime.List'2.stail'7,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List()))))))),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(App(Free(collectA'37,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Leon_Runtime.List'2,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))))),Free(x'35,Type(Int.int,List()))),App(Const(Leon_Runtime.List'2.stail'7,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List()))))))))),Abs(x'd'1'1223,Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List()))))),App(App(Const(HOL.Let,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),Bound(0))),Abs(b2'1227,Type(Int.int,List()),App(App(Const(HOL.Let,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),Bound(1)))),Abs(c2'1228,Type(Int.int,List()),App(App(Const(HOL.Let,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),Bound(2)))),Abs(l2'1229,Type(Leon_Runtime.List'2,List()),App(App(Const(Product_Type.Pair,Type(dummy,List())),App(App(Const(Leon_Runtime.max'34,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Int.int,List()), Type(Int.int,List())))))),App(Const(Leon_Runtime.List'2.sb'5,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),Bound(2))),App(App(Const(Product_Type.Pair,Type(dummy,List())),App(App(Const(Leon_Runtime.max'34,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Int.int,List()), Type(Int.int,List())))))),App(Const(Leon_Runtime.List'2.sc'6,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),Bound(1))),Bound(0)))))))))))),App(App(App(Const(HOL.If,Type(dummy,List())),App(App(Const(HOL.conj,Type(dummy,List())),App(Const(Leon_Runtime.List'2.dCons'3,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),App(Const(HOL.Not,Type(dummy,List())),App(App(Const(HOL.eq,Type(dummy,List())),App(Const(Leon_Runtime.List'2.sa'4,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),Free(x'35,Type(Int.int,List())))))),App(App(Const(HOL.Let,Type(dummy,List())),App(App(Const(Product_Type.Pair,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),App(App(Free(collectA'37,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Leon_Runtime.List'2,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))))),Free(x'35,Type(Int.int,List()))),App(Const(Leon_Runtime.List'2.stail'7,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))))),App(App(Const(Product_Type.Pair,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),App(App(Free(collectA'37,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Leon_Runtime.List'2,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))))),Free(x'35,Type(Int.int,List()))),App(Const(Leon_Runtime.List'2.stail'7,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List()))))))),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(App(Free(collectA'37,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Leon_Runtime.List'2,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))))),Free(x'35,Type(Int.int,List()))),App(Const(Leon_Runtime.List'2.stail'7,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List()))))))))),Abs(x'd'2'1234,Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List()))))),App(App(Const(HOL.Let,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),Bound(0))),Abs(b2'1238,Type(Int.int,List()),App(App(Const(HOL.Let,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),Bound(1)))),Abs(c2'1239,Type(Int.int,List()),App(App(Const(HOL.Let,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),Bound(2)))),Abs(l2'1240,Type(Leon_Runtime.List'2,List()),App(App(Const(Product_Type.Pair,Type(dummy,List())),Bound(2)),App(App(Const(Product_Type.Pair,Type(dummy,List())),Bound(1)),App(App(App(App(Const(Leon_Runtime.List'2.cCons'3,Type(dummy,List())),App(Const(Leon_Runtime.List'2.sa'4,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),App(Const(Leon_Runtime.List'2.sb'5,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),App(Const(Leon_Runtime.List'2.sc'6,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),Bound(0))))))))))))),App(Const(Leon_Library.error,Type(fun,List(Type(dummy,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))),App(Const(Num.numeral_class.numeral,Type(fun,List(Type(Num.num,List()), Type(Nat.nat,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),Const(Num.num.One,Type(Num.num,List()))))))))))))))))))))))))))),Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List()))))))))
[Internal] Please inform the authors of Leon about this message