diff --git a/src/driver.rs b/src/driver.rs
index a8003cbd..82a213bf 100644
--- a/src/driver.rs
+++ b/src/driver.rs
@@ -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 {
@@ -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 {
@@ -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 {
diff --git a/src/main.rs b/src/main.rs
index 2a29cfc5..9e91d9ba 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -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)