Skip to content

Commit

Permalink
Merge pull request #730 from viperproject/meilers_fix_silicon_742
Browse files Browse the repository at this point in the history
Added missing case (fixes Silicon issue #742)
  • Loading branch information
marcoeilers authored Aug 14, 2023
2 parents 04df2df + 948b7e9 commit 501f1ec
Show file tree
Hide file tree
Showing 2 changed files with 29 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
case PMapType(_, _) => Seq("Map")
case PDomainType(d, _) if d.name == "PredicateInstance" => Seq("PredicateInstances")
case PDomainType(d, _) => Seq(d.name)
case gt: PGenericType => Seq(gt.genericName)
}
!typeNames.exists(tn => wfTypeName.contains(tn))
}
Expand Down
28 changes: 28 additions & 0 deletions src/test/resources/all/issues/silicon/0742.vpr
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

import <decreases/all.vpr>

domain ListWellFoundedOrder[T] {


axiom {
forall y : List[T] :: {bounded(y)} bounded(y)
}


axiom {
forall xs : List[T] , y : T ::
decreasing(xs, Cons(y, xs))
}

axiom {
forall xs : List[T], ys : List[T], zs : List[T] :: {decreasing(xs, ys), decreasing(ys, zs)}
decreasing(xs, ys) && decreasing(ys, zs) ==> decreasing(xs, zs)
}
}

adt List[T] {
Nil()
Cons(value : T, tail : List[T])
}

0 comments on commit 501f1ec

Please sign in to comment.