Lemmas containing composed sorts are not parsed correctly

mattulbrich commented 3 years ago

The following lemma raises an exception.

lemma l1(s: seq<int>) ensures (|s|==|s|) {}

The stacktrace is essentially:

java.lang.ArrayIndexOutOfBoundsException: Index 0 out of bounds for length 0
    at edu.kit.iti.algover.util.Util$ReadOnlyArrayList.get(Util.java:457)
    at edu.kit.iti.algover.term.builder.TreeTermTranslator.buildCardinality(TreeTermTranslator.java:868)
    at edu.kit.iti.algover.term.builder.TreeTermTranslator.build(TreeTermTranslator.java:467)
    at edu.kit.iti.algover.rules.DafnyRuleUtil.generateRule(DafnyRuleUtil.java:175)
    at edu.kit.iti.algover.rules.DafnyRuleUtil.generateDafnyRules(DafnyRuleUtil.java:70)
    at edu.kit.iti.algover.project.Project.makeLemmaProofRules(Project.java:442)

mattulbrich commented 3 years ago

I have added a failing test case on the branch fix-192.

JonasKlamroth commented 3 years ago

@mattulbrich i had to adapt you testcase slightly but i figured that this is still the fix you were looking for. can you confirm? if so pls consider merging

mattulbrich / dive

Lemmas containing composed sorts are not parsed correctly #192