Test all/assume/assume10QPpred.sil causes Boogie errors

[viper-admin]

Created by @mschwerhoff on 2018-10-12 13:31 Last updated on 2019-08-28 13:03

all/assume/assume10QPpred.sil [carbon-Silver] *** FAILED *** (1 second, 219 milliseconds)
13 errors

The following output occurred during testing, but should not have according to the test annotations:
  [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: 12 name resolution errors detected in C:\Users\scmalte.D\AppData\Local\Temp\carbon3480321951534693585.bpl (<no position>)
  [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: C:\Users\scmalte.D\AppData\Local\Temp\carbon3480321951534693585.bpl(718,8): Error: trigger must mention all quantified variables, but does not mention: z_1 (<no position>)
  [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: C:\Users\scmalte.D\AppData\Local\Temp\carbon3480321951534693585.bpl(718,8): Error: trigger must mention all quantified variables, but does not mention: y_1 (<no position>)
  [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: C:\Users\scmalte.D\AppData\Local\Temp\carbon3480321951534693585.bpl(717,43): Error: more than one declaration of variable name: z_1 (<no position>)
  [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: C:\Users\scmalte.D\AppData\Local\Temp\carbon3480321951534693585.bpl(717,33): Error: more than one declaration of variable name: y_1 (<no position>)
  [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: C:\Users\scmalte.D\AppData\Local\Temp\carbon3480321951534693585.bpl(708,8): Error: trigger must mention all quantified variables, but does not mention: z_1 (<no position>)
  [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: C:\Users\scmalte.D\AppData\Local\Temp\carbon3480321951534693585.bpl(708,8): Error: trigger must mention all quantified variables, but does not mention: y_1 (<no position>)
  [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: C:\Users\scmalte.D\AppData\Local\Temp\carbon3480321951534693585.bpl(707,43): Error: more than one declaration of variable name: z_1 (<no position>)
  [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: C:\Users\scmalte.D\AppData\Local\Temp\carbon3480321951534693585.bpl(707,33): Error: more than one declaration of variable name: y_1 (<no position>)
  [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: C:\Users\scmalte.D\AppData\Local\Temp\carbon3480321951534693585.bpl(697,8): Error: trigger must mention all quantified variables, but does not mention: z_1 (<no position>)
  [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: C:\Users\scmalte.D\AppData\Local\Temp\carbon3480321951534693585.bpl(697,8): Error: trigger must mention all quantified variables, but does not mention: y_1 (<no position>)
  [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: C:\Users\scmalte.D\AppData\Local\Temp\carbon3480321951534693585.bpl(696,43): Error: more than one declaration of variable name: z_1 (<no position>)
  [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: C:\Users\scmalte.D\AppData\Local\Temp\carbon3480321951534693585.bpl(696,33): Error: more than one declaration of variable name: y_1 (<no position>) (AnnotationBasedTestSuite.scala:64)

[viper-admin]

@marcoeilers commented on 2019-08-28 13:03

This no longer causes Boogie errors, but assertions cannot be proved even though they apparently should, so I’ll leave this open.