Skip to content

Commit

Permalink
remove unnecessary references
Browse files Browse the repository at this point in the history
  • Loading branch information
Philipp15b committed Dec 21, 2024
1 parent 96241d3 commit 2497e5f
Show file tree
Hide file tree
Showing 2 changed files with 11 additions and 5 deletions.
6 changes: 3 additions & 3 deletions src/driver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -676,7 +676,7 @@ impl<'ctx> SmtVcUnit<'ctx> {

let smtlib = get_smtlib(options, &prover);
if let Some(smtlib) = &smtlib {
write_smtlib(&options.debug_options, name, &smtlib, None)?;
write_smtlib(&options.debug_options, name, smtlib, None)?;
}

if options.debug_options.no_verify {
Expand Down Expand Up @@ -737,7 +737,7 @@ impl<'ctx> SmtVcUnit<'ctx> {
smt_dir: options.debug_options.smt_dir.clone(),
..options.debug_options
};
write_smtlib(&options, name, &smtlib, Some(&result))?;
write_smtlib(&options, name, smtlib, Some(&result))?;
}

Ok(SmtVcCheckResult {
Expand Down Expand Up @@ -808,7 +808,7 @@ fn write_smtlib<'ctx>(
let mut smtlib = smtlib.clone();
smtlib.add_check_sat();
if let Some(prove_result) = prove_result {
smtlib.add_details_query(&prove_result);
smtlib.add_details_query(prove_result);
}
let smtlib = smtlib.into_string();
if options.print_smt {
Expand Down
10 changes: 8 additions & 2 deletions src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -708,8 +708,14 @@ fn verify_files_main(
}

// 13. Create Z3 solver with axioms, solve
let mut result =
vc_is_valid.run_solver(options, &limits_ref,name, &ctx, &mut translate, &slice_vars)?;
let mut result = vc_is_valid.run_solver(
options,
&limits_ref,
name,
&ctx,
&mut translate,
&slice_vars,
)?;

server
.handle_vc_check_result(name, verify_unit.span, &mut result, &mut translate)
Expand Down

0 comments on commit 2497e5f

Please sign in to comment.