Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add script to run Boogie with the args Dafny uses #4492

Open
wants to merge 14 commits into
base: master
Choose a base branch
from
Prev Previous commit
Next Next commit
Move boogie-args.cfg
  • Loading branch information
atomb committed Jan 8, 2024
commit 575e8f10296f25d1880abd26c4ef62473e984a99
2 changes: 1 addition & 1 deletion Scripts/dafny_boogie.sh
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#!/bin/bash
ROOT=$(dirname $(dirname "${BASH_SOURCE[0]}"))
BOOGIE_ARGS=$(sed -e 's|^|-|' "${ROOT}"/Test/boogie-args.cfg | sed -e "s|{ROOT}|$ROOT|")
BOOGIE_ARGS=$(sed -e 's|^|-|' "${ROOT}"/Source/boogie-args.cfg | sed -e "s|{ROOT}|$ROOT|")
dotnet tool run boogie $BOOGIE_ARGS "$@"
2 changes: 1 addition & 1 deletion Source/IntegrationTests/LitTests.cs
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ public class LitTests {
};

DefaultBoogieArguments =
File.ReadAllLines(RepositoryRoot + "Test/boogie-args.cfg")
File.ReadAllLines(RepositoryRoot + "Source/boogie-args.cfg")
.Select(arg => "-" + arg)
.Append("/proverOpt:PROVER_PATH:" + RepositoryRoot + $"../unzippedRelease/dafny/z3/bin/z3-{DafnyOptions.DefaultZ3Version}")
.ToArray();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -147,7 +147,7 @@ dafnyArgs = [
]

boogieArgs = ""
with open(repositoryRoot + '/Test/boogie-args.cfg', 'r') as boogieArgFile:
with open(repositoryRoot + '/Source/boogie-args.cfg', 'r') as boogieArgFile:
boogieArgs = boogieArgFile.read().splitlines() + ["proverOpt:PROVER_PATH=" + solverPath]

# Add standard parameters
Expand Down
File renamed without changes.
Loading