Merge branch 'main' into sam/hashset

data-structures/maps/mutablemaps/stainless.conf

@@ -14,3 +14,4 @@ solvers             = "smt-cvc5,smt-z3,smt-cvc4"
 check-measures      = yes
 infer-measures      = true
 simplifier           = "ol"
+compact              = true

lexers/regex/verifiedlexer/stainless.conf

@@ -13,3 +13,4 @@ solvers             = "smt-cvc5,smt-z3,smt-cvc4"
 check-measures      = yes
 infer-measures      = true
 simplifier           = "bland"
+compact             = true

run-one-test.sh

@@ -13,6 +13,7 @@ function run_tests {
     conf=stainless.conf.nightly
   fi
   echo ""
+  echo `date`
   echo "------------------------------------------------------------------------------------------"
   # Check if there is a verify.sh file in the project folder
   # If yes, then echo a message saying we run it and its content, then run it, other run the command X
@@ -45,4 +46,4 @@ function run_tests {
   echo ""
 }
 
-run_tests "${@:2}"
+run_tests "${@:2}"

stainless.conf.nightly

@@ -1,6 +1,6 @@
-vc-cache = false
 timeout = 300
 fail-early = true
 strict-arithmetic = false
 solvers="smt-z3"
 no-colors=true
+compact=true

tutorials/const-fold/ConstFold.scala

@@ -3,16 +3,16 @@ import stainless.lang.{ghost => ghostExpr, *}
 object ConstFold:
 
   sealed abstract class Expr
-  case class Number(value: Int) extends Expr
+  case class Number(value: BigInt) extends Expr
   case class Var(name: String) extends Expr
   case class Add(e1: Expr, e2: Expr) extends Expr
   case class Minus(e1: Expr, e2: Expr) extends Expr
   case class Mul(e1: Expr, e2: Expr) extends Expr
 
-  type Env = String => Int
-  val zeroEnv = (_:String) => 0
+  type Env = String => BigInt
+  val zeroEnv: Env = (_:String) => BigInt(0)
 
-  def evaluate(ctx: Env, e: Expr): Int = 
+  def evaluate(ctx: Env, e: Expr): BigInt = 
     e match
       case Number(value) => value
       case Var(name) => ctx(name)

tutorials/const-fold/stainless.conf

@@ -1,5 +1,5 @@
 strict-arithmetic = false
-timeout = 15
+timeout = 25
 compact = true
 no-colors = true
 solvers = smt-cvc5