From 6a4a0cb9593279ce5c81d5344cafe103d881968e Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Fri, 23 Aug 2024 18:12:04 +0200 Subject: [PATCH] with lemma --- asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala | 2 +- asn1scala/stainless.conf | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala index 09c799ff..11bf44c3 100644 --- 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 index b0919113..eaeb7016 100644 --- 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