search

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
349 stars 50 forks source link

Finite sets printed in debug using curly braces instead of Set(...) #1544

Closed vkuncak closed 1 month ago

vkuncak commented 1 month ago

Printing trees with command

stainless Vector.scala --solvers=smt-cvc5 --timeout=3 --watch --debug=trees --debug-phases=TypeEncoding

I noticed this printout, which uses abbreviated set notation, but I think we should use normal Scala parsable notation for sets:

[ Debug  ] @library
[ Debug  ] def content[T](thiss: List[T]): Set[T] = thiss match {
[ Debug  ]   case Nil() =>
[ Debug  ]     {}
[ Debug  ]   case Cons(h, t) =>
[ Debug  ]     {h} ++ content[T](t)
[ Debug  ] }
vkuncak commented 1 month ago

Fixed by https://github.com/epfl-lara/inox/pull/216

vkuncak commented 1 month ago

https://github.com/epfl-lara/inox/pull/216