## For Boogie 2012-10-22 with Z3 4.3.0: time -p boogie tournament.bpl > tournament.log ## For Boogie 2011-03-17 with Z3 2.15: # time -p boogie /errorLimit:1 /trace /traceTimes /traceverify /errorTrace:2 /logInfer /bv:n /proverMemoryLimit:6000 /z3opt:memory:6000 /vcsMaxCost:0 /vcsMaxSplits:1000 /vcsMaxKeepGoingSplits:100 /vcsKeepGoingTimeout:5000 /vcsFinalAssertTimeout:10000 tournament.bpl > tournament.log # time -p boogie /errorLimit:1 /trace /traceTimes /traceverify /errorTrace:2 /logInfer /bv:n /proverMemoryLimit:6000 /z3opt:memory:6000 /vcsMaxCost:0 /vcsMaxSplits:1000 /vcsMaxKeepGoingSplits:100 /vcsKeepGoingTimeout:5000 /vcsFinalAssertTimeout:10000 tournament.bpl > tournament.log # time -p boogie /errorLimit:1 /trace /traceTimes /traceverify /errorTrace:2 /logInfer /bv:n /proverMemoryLimit:6000 /z3opt:memory:6000 /vcsMaxCost:0 /vcsMaxSplits:1000 /vcsMaxKeepGoingSplits:100 /vcsKeepGoingTimeout:5000 /vcsFinalAssertTimeout:10000 /restartProver tournament.bpl > tournament.log # time -p boogie /errorLimit:1 /trace /traceTimes /traceverify /errorTrace:2 /logInfer /bv:n /proverMemoryLimit:6000 /z3opt:memory:6000 tournament.bpl > tournament.log # time -p boogie /errorLimit:1 /trace /traceTimes /traceverify /errorTrace:2 /logInfer /bv:n /proverMemoryLimit:6000 /z3opt:memory:6000 /restartProver tournament.bpl > tournament.log