Skip to content

Commit

Permalink
[move-prover] update cvc4 to cvc5 as boogie solver option
Browse files Browse the repository at this point in the history
Boogie 2.9.6 does not recognize CVC4, used CVC5 instead.
  • Loading branch information
meng-xu-cs authored and bors-libra committed Nov 18, 2021
1 parent 24e014a commit a992689
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion language/move-prover/boogie-backend/src/options.rs
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ impl BoogieOptions {
add(DEFAULT_BOOGIE_FLAGS);
if self.use_cvc4 {
add(&[
"-proverOpt:SOLVER=cvc4",
"-proverOpt:SOLVER=cvc5",
&format!("-proverOpt:PROVER_PATH={}", &self.cvc4_exe),
]);
} else {
Expand Down

0 comments on commit a992689

Please sign in to comment.