diff --git a/src/main/scala/inox/Main.scala b/src/main/scala/inox/Main.scala index e19602e404d43a5399bcbb4bbc27d1894d43fc45..490b78d7a7f944622d8ec587d64215c41e7cd2e3 100644 --- a/src/main/scala/inox/Main.scala +++ b/src/main/scala/inox/Main.scala @@ -33,7 +33,7 @@ trait MainHelpers { protected def getOptions: Map[OptionDef[_], String] = Map( optTimeout -> "Set a timeout for each proof attempt (in sec.)", optSelectedSolvers -> { - "Use solvers s1, s2,...\nAvailable: " + + "Use solvers s1,s2,...\nAvailable: " + solvers.SolverFactory.solverNames.toSeq.sortBy(_._1).map { case (name, desc) => f"\n $name%-14s : $desc" } diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala index a9491af7ce403e0162f9edb2e7f09e25202e2905..86ef28e9d6686f29ecf194d93e70d9d908482270 100644 --- a/src/main/scala/inox/ast/Definitions.scala +++ b/src/main/scala/inox/ast/Definitions.scala @@ -178,6 +178,10 @@ trait Definitions { self: Trees => case _ => Annotation(name, args) } + implicit class FlagSetWrapper(flags: Set[Flag]) { + def contains(str: String): Boolean = flags contains Annotation(str, Seq.empty) + } + /** Represents an ADT definition (either the ADT sort or a constructor). */ sealed trait ADTDefinition extends Definition { val id: Identifier