stainless-dotty \
src/main/scala/asn1scala/asn1jvm.scala  \
src/main/scala/asn1scala/asn1jvm_Verification.scala  \
src/main/scala/asn1scala/asn1jvm_Helper.scala \
src/main/scala/asn1scala/asn1jvm_Bitstream.scala \
src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala \
src/main/scala/asn1scala/asn1jvm_Vector.scala \
src/main/scala/asn1scala/asn1jvm_Codec.scala \
--config-file=stainless.conf \
-D-parallel=5 \
--functions=initACNCodec,reader,dec_Int_PositiveInteger_ConstSize_big_endian_16_prefixLemma,dec_Int_PositiveInteger_ConstSize_big_endian_32_prefixLemma,dec_Int_PositiveInteger_ConstSize_big_endian_64_prefixLemma,dec_Int_PositiveInteger_ConstSize_little_endian_16_prefixLemma,dec_Int_PositiveInteger_ConstSize_little_endian_32_prefixLemma,dec_Int_PositiveInteger_ConstSize_little_endian_64_prefixLemma,enc_Int_PositiveInteger_ConstSize,enc_Int_PositiveInteger_ConstSize,resetAt,withMovedByteIndex,withMovedBitIndex,isPrefixOf,enc_Int_PositiveInteger_ConstSize_8,enc_Int_PositiveInteger_ConstSize_big_endian_16,enc_Int_PositiveInteger_ConstSize_big_endian_32,enc_Int_PositiveInteger_ConstSize_big_endian_64,dec_Int_PositiveInteger_ConstSize,dec_Int_PositiveInteger_ConstSize_pure,dec_Int_PositiveInteger_ConstSize_8,dec_Int_PositiveInteger_ConstSize_8_pure,dec_Int_PositiveInteger_ConstSize_big_endian_16,dec_Int_PositiveInteger_ConstSize_big_endian_16_pure,dec_Int_PositiveInteger_ConstSize_big_endian_32,dec_Int_PositiveInteger_ConstSize_big_endian_32_pure,dec_Int_PositiveInteger_ConstSize_big_endian_64,dec_Int_PositiveInteger_ConstSize_big_endian_64_pure,dec_Int_PositiveInteger_ConstSize_little_endian_16_pure,dec_Int_PositiveInteger_ConstSize_little_endian_32_pure,dec_Int_PositiveInteger_ConstSize_little_endian_64_pure,enc_Int_TwosComplement_ConstSize,enc_Int_TwosComplement_ConstSize_8,enc_Int_TwosComplement_ConstSize_big_endian_16,enc_Int_TwosComplement_ConstSize_big_endian_32,enc_Int_TwosComplement_ConstSize_big_endian_64,dec_Int_TwosComplement_ConstSize,dec_Int_TwosComplement_ConstSize_pure,dec_Int_TwosComplement_ConstSize_8,dec_Int_TwosComplement_ConstSize_big_endian_16,dec_Int_TwosComplement_ConstSize_big_endian_32,dec_Int_TwosComplement_ConstSize_big_endian_64,BitStream_ReadBitPattern,BitStream_DecodeTrueFalseBoolean,enc_Real_IEEE754_32_big_endian,enc_Real_IEEE754_32_little_endian,enc_Real_IEEE754_64_big_endian,enc_Real_IEEE754_64_little_endian,dec_Real_IEEE754_32_big_endian,dec_Real_IEEE754_32_little_endian,dec_Real_IEEE754_64_big_endian,dec_Real_IEEE754_64_little_endian,enc_String_Ascii_Null_Terminated_multVec,enc_String_CharIndex_private,enc_IA5String_CharIndex_External_Field_Determinant,enc_IA5String_CharIndex_External_Field_DeterminantVec,enc_IA5String_CharIndex_Internal_Field_DeterminantVec,dec_String_Ascii_Null_Terminated_multVec,dec_String_CharIndex_private,dec_IA5String_CharIndex_External_Field_Determinant,dec_IA5String_CharIndex_External_Field_DeterminantVec,dec_IA5String_CharIndex_Internal_Field_Determinant,dec_IA5String_CharIndex_Internal_Field_DeterminantVec,milbus_encode,milbus_decode \
$1
