Skip to content

Commit e9529ac

Browse files
committed
Changes needed for minimal support for Boogie 3.5 for TACAS
1 parent a321447 commit e9529ac

File tree

2 files changed

+2
-3
lines changed

2 files changed

+2
-3
lines changed

bin/versions

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
Z3_VERSION="4.8.12"
22
CVC4_VERSION="1.8"
33
YICES2_VERSION="2.6.2"
4-
BOOGIE_VERSION="2.9.6"
4+
BOOGIE_VERSION="3.5.1"
55
CORRAL_VERSION="1.1.8"
66
SYMBOOGLIX_COMMIT="ccb2e7f2b3"
77
LOCKPWN_COMMIT="12ba58f1ec"

share/smack/top.py

+1-2
Original file line numberDiff line numberDiff line change
@@ -936,8 +936,7 @@ def verification_result(verifier_output, verifier):
936936
def boogie_command(args):
937937
command = ["boogie"]
938938
command += [args.bpl_file]
939-
command += ["/doModSetAnalysis"]
940-
command += ["/useArrayTheory"]
939+
command += ["/inferModifies"]
941940
command += ["/timeLimit:%s" % args.time_limit]
942941
command += ["/errorLimit:%s" % args.max_violations]
943942
if not args.modular:

0 commit comments

Comments
 (0)