Skip to content

Commit d6c9c74

Browse files
authored
Update to Boogie 2.15.9 (#441)
1 parent 927205b commit d6c9c74

2 files changed

Lines changed: 3 additions & 2 deletions

File tree

.github/workflows/ci.yml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ jobs:
1414
container: gobraverifier/gobra-base:v5_z3_4.8.7 # Thank you, Gobra team
1515
env:
1616
BOOGIE_EXE: "boogie/Boogie"
17-
LINUX_BOOGIE_URL: "https://github.com/viperproject/boogie-builder/releases/download/bae82d3a7b383161/boogie-linux.zip"
17+
LINUX_BOOGIE_URL: "https://github.com/viperproject/boogie-builder/releases/download/7449a7a899c02c95/boogie-linux.zip"
1818
steps:
1919
- name: Checkout Carbon
2020
uses: actions/checkout@v2
@@ -57,6 +57,7 @@ jobs:
5757
unzip boogie-linux.zip
5858
rm -rf boogie-linux.zip
5959
mv binaries-linux boogie
60+
boogie/Boogie /version
6061
pwd
6162
6263
- name: Test Carbon

src/main/scala/viper/carbon/boogie/BoogieNameGenerator.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ class BoogieNameGenerator extends DefaultNameGenerator {
1919
"invariant", "goto", "break", "return", "call", "forall", "assert", "havoc", "assume", "returns", "var", "implementation",
2020
"axiom", "exists", "old", "false", "real", "int", "true", "bool", "finite", "ensures", "requires", "modifies", "where", "par", "lambda",
2121
"uses", "RTP", "RTZ", "yield", "async", "roundNearestTiesToAway", "roundNearestTiesToEven", "extends", "roundTowardPositive",
22-
"roundTowardZero", "RNA", "RTN", "roundTowardNegative", "RNE") ++
22+
"roundTowardZero", "RNA", "RTN", "roundTowardNegative", "RNE", "is") ++
2323
Set("Set", "MultiSet", "Seq")
2424
val SMTreservedNames: Set[String] = Set(
2525
// Basic symbols:

0 commit comments

Comments
 (0)