smt: write smt-lib files also before smt call, add --no-verify option

src/driver.rs

@@ -53,7 +53,7 @@ use crate::{
         vcgen::Vcgen,
     },
     version::write_detailed_version_info,
-    Options, SliceOptions, SliceVerifyMethod, VerifyError,
+    DebugOptions, Options, SliceOptions, SliceVerifyMethod, VerifyError,
 };
 
 use ariadne::ReportKind;
@@ -65,7 +65,7 @@ use z3::{
 use z3rro::{
     prover::{ProveResult, Prover},
     smtlib::Smtlib,
-    util::PrefixWriter,
+    util::{PrefixWriter, ReasonUnknown},
 };
 
 use tracing::{info_span, instrument, trace};
@@ -664,6 +664,7 @@ impl<'ctx> SmtVcUnit<'ctx> {
         self,
         options: &Options,
         limits_ref: &LimitsRef,
+        name: &SourceUnitName,
         ctx: &'ctx Context,
         translate: &mut TranslateExprs<'smt, 'ctx>,
         slice_vars: &SliceStmts,
@@ -672,7 +673,21 @@ impl<'ctx> SmtVcUnit<'ctx> {
         let _entered = span.enter();
 
         let prover = mk_valid_query_prover(limits_ref, ctx, translate, &self.vc);
+
         let smtlib = get_smtlib(options, &prover);
+        if let Some(smtlib) = &smtlib {
+            write_smtlib(&options.debug_options, name, &smtlib, None)?;
+        }
+
+        if options.debug_options.no_verify {
+            return Ok(SmtVcCheckResult {
+                prove_result: ProveResult::Unknown(ReasonUnknown::Other(
+                    "verification skipped".to_owned(),
+                )),
+                quant_vc: self.quant_vc,
+                slice_model: None,
+            });
+        }
 
         let mut slice_solver = SliceSolver::new(slice_vars.clone(), translate, prover);
         let failing_slice_options = SliceSolveOptions {
@@ -715,11 +730,20 @@ impl<'ctx> SmtVcUnit<'ctx> {
             }
         }
 
+        if let Some(smtlib) = &smtlib {
+            // only print to the directory again
+            let options = DebugOptions {
+                print_smt: false,
+                smt_dir: options.debug_options.smt_dir.clone(),
+                ..options.debug_options
+            };
+            write_smtlib(&options, name, &smtlib, Some(&result))?;
+        }
+
         Ok(SmtVcCheckResult {
             prove_result: result,
             quant_vc: self.quant_vc,
             slice_model,
-            smtlib,
         })
     }
 }
@@ -773,12 +797,45 @@ fn get_smtlib(options: &Options, prover: &Prover) -> Option<Smtlib> {
     }
 }
 
+/// Write the SMT-LIB dump to a file if requested.
+fn write_smtlib<'ctx>(
+    options: &DebugOptions,
+    name: &SourceUnitName,
+    smtlib: &Smtlib,
+    prove_result: Option<&ProveResult<'ctx>>,
+) -> Result<(), VerifyError> {
+    if options.print_smt || options.smt_dir.is_some() {
+        let mut smtlib = smtlib.clone();
+        smtlib.add_check_sat();
+        if let Some(prove_result) = prove_result {
+            smtlib.add_details_query(&prove_result);
+        }
+        let smtlib = smtlib.into_string();
+        if options.print_smt {
+            println!("\n; --- Solver SMT-LIB ---\n{}\n", smtlib);
+        }
+        if let Some(smt_dir) = &options.smt_dir {
+            let file_path = smt_dir.join(name.to_file_name("smt2"));
+            create_dir_all(file_path.parent().unwrap())?;
+            let mut file = File::create(&file_path)?;
+            let mut comment_writer = PrefixWriter::new("; ".as_bytes(), &mut file);
+            write_detailed_version_info(&mut comment_writer)?;
+            writeln!(comment_writer, "Source unit: {}", name)?;
+            if let Some(prove_result) = prove_result {
+                writeln!(comment_writer, "Prove result: {}", &prove_result)?;
+            }
+            file.write_all(smtlib.as_bytes())?;
+            tracing::info!(?file_path, "SMT-LIB query written to file");
+        }
+    }
+    Ok(())
+}
+
 /// The result of an SMT solver call for a [`SmtVcUnit`].
 pub struct SmtVcCheckResult<'ctx> {
     pub prove_result: ProveResult<'ctx>,
     slice_model: Option<SliceModel>,
     quant_vc: QuantVcUnit,
-    smtlib: Option<Smtlib>,
 }
 
 impl<'ctx> SmtVcCheckResult<'ctx> {
@@ -901,33 +958,4 @@ impl<'ctx> SmtVcCheckResult<'ctx> {
 
         Ok(())
     }
-
-    /// Write the SMT-LIB dump to a file if requested.
-    pub fn write_smtlib(
-        &self,
-        options: &Options,
-        name: &SourceUnitName,
-    ) -> Result<(), VerifyError> {
-        if options.debug_options.print_smt || options.debug_options.smt_dir.is_some() {
-            let mut smtlib = self.smtlib.clone().unwrap();
-            smtlib.add_check_sat();
-            smtlib.add_details_query(&self.prove_result);
-            let smtlib = smtlib.into_string();
-            if options.debug_options.print_smt {
-                println!("\n; --- Solver SMT-LIB ---\n{}\n", smtlib);
-            }
-            if let Some(smt_dir) = &options.debug_options.smt_dir {
-                let file_path = smt_dir.join(name.to_file_name("smt2"));
-                create_dir_all(file_path.parent().unwrap())?;
-                let mut file = File::create(&file_path)?;
-                let mut comment_writer = PrefixWriter::new("; ".as_bytes(), &mut file);
-                write_detailed_version_info(&mut comment_writer)?;
-                writeln!(comment_writer, "Source unit: {}", name)?;
-                writeln!(comment_writer, "Prove result: {}", self.prove_result)?;
-                file.write_all(smtlib.as_bytes())?;
-                tracing::info!(?file_path, "SMT-LIB query written to file");
-            }
-        }
-        Ok(())
-    }
 }

src/main.rs

@@ -140,8 +140,9 @@ pub struct OptimizationOptions {
     #[arg(long)]
     pub egraph: bool,
 
-    /// Don't do reachability checks during unfolding of verification conditions
-    /// to eliminate unreachable branches. Instead, unfold all branches.
+    /// Don't do SMT-powered reachability checks during unfolding of
+    /// verification conditions to eliminate unreachable branches. Instead,
+    /// unfold all branches.
     #[arg(long)]
     pub strict: bool,
 
@@ -223,6 +224,11 @@ pub struct DebugOptions {
     #[arg(long)]
     pub no_pretty_smtlib: bool,
 
+    /// Do not run the final SMT check to verify the program. This is useful to
+    /// obtain just the SMT-LIB output.
+    #[arg(long)]
+    pub no_verify: bool,
+
     /// Enable Z3 tracing for the final SAT check.
     #[arg(long)]
     pub z3_trace: bool,
@@ -703,15 +709,12 @@ fn verify_files_main(
 
         // 13. Create Z3 solver with axioms, solve
         let mut result =
-            vc_is_valid.run_solver(options, &limits_ref, &ctx, &mut translate, &slice_vars)?;
+            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)
             .map_err(VerifyError::ServerError)?;
 
-        // If requested, write the SMT-LIB output.
-        result.write_smtlib(options, name)?;
-
         if options.debug_options.z3_trace {
             info!("Z3 tracing output will be written to `z3.log`.");
         }