with lemma

esa · Aug 23, 2024 · 6a4a0cb · 6a4a0cb
1 parent ae41167
commit 6a4a0cb
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala
@@ -984,7 +984,7 @@ case class BitStream private [asn1scala](
 
             assert(r3Got_23 == r3_23)
 
-            // checkBitsLoopPrefixLemma(r1_13, nBits, bit, from) // not needed but speed up verification
+            checkBitsLoopPrefixLemma(r1_13, nBits, bit, from) // not needed but speed up verification
             assert(r2_23 == r1_13.withMovedBitIndex(1))
             check(resGot_13 == resGot_23) // timeout
             check(r3Got_13 == r3_13)

diff --git a/asn1scala/stainless.conf b/asn1scala/stainless.conf
@@ -12,5 +12,5 @@ strict-arithmetic   = true
 solvers             = "smt-cvc5,smt-z3,smt-cvc4"
 check-measures      = yes
 infer-measures      = true
-simplifier           = "ol"
+simplifier           = "bland"
 no-colors           = false