diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 819ffed5..735a2e3c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -14,7 +14,7 @@ jobs: container: gobraverifier/gobra-base:v5_z3_4.8.7 # Thank you, Gobra team env: BOOGIE_EXE: "boogie/Boogie" - LINUX_BOOGIE_URL: "https://github.com/viperproject/boogie-builder/releases/download/bae82d3a7b383161/boogie-linux.zip" + LINUX_BOOGIE_URL: "https://github.com/viperproject/boogie-builder/releases/download/7449a7a899c02c95/boogie-linux.zip" steps: - name: Checkout Carbon uses: actions/checkout@v2 @@ -57,6 +57,7 @@ jobs: unzip boogie-linux.zip rm -rf boogie-linux.zip mv binaries-linux boogie + boogie/Boogie /version pwd - name: Test Carbon diff --git a/src/main/scala/viper/carbon/boogie/BoogieNameGenerator.scala b/src/main/scala/viper/carbon/boogie/BoogieNameGenerator.scala index 0ac0a96e..6c9bfb88 100644 --- a/src/main/scala/viper/carbon/boogie/BoogieNameGenerator.scala +++ b/src/main/scala/viper/carbon/boogie/BoogieNameGenerator.scala @@ -19,7 +19,7 @@ class BoogieNameGenerator extends DefaultNameGenerator { "invariant", "goto", "break", "return", "call", "forall", "assert", "havoc", "assume", "returns", "var", "implementation", "axiom", "exists", "old", "false", "real", "int", "true", "bool", "finite", "ensures", "requires", "modifies", "where", "par", "lambda", "uses", "RTP", "RTZ", "yield", "async", "roundNearestTiesToAway", "roundNearestTiesToEven", "extends", "roundTowardPositive", - "roundTowardZero", "RNA", "RTN", "roundTowardNegative", "RNE") ++ + "roundTowardZero", "RNA", "RTN", "roundTowardNegative", "RNE", "is") ++ Set("Set", "MultiSet", "Seq") val SMTreservedNames: Set[String] = Set( // Basic symbols: