.forgejo/workflows/test.yml

@@ -30,7 +30,6 @@ jobs:
             lld \
             pkg-config \
             python3 \
-            python3-click \
             tcl-dev \
             z3 \
             zlib1g-dev \

crates/fayalite/src/cli.rs

@@ -419,8 +419,8 @@ pub struct FormalArgs {
     pub mode: FormalMode,
     #[arg(long, default_value_t = Self::DEFAULT_DEPTH)]
     pub depth: u64,
-    #[arg(long, default_value = "z3")]
+    #[arg(long)]
-    pub solver: String,
+    pub solver: Option<String>,
     #[arg(long)]
     pub smtbmc_extra_args: Vec<String>,
     #[command(flatten)]
@@ -479,6 +479,18 @@ impl FormalArgs {
             solver,
             _formal_adjust_args: _,
         } = self;
+        struct OptArg<T>(Option<T>);
+        impl<T: fmt::Display> fmt::Display for OptArg<T> {
+            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+                if let Some(v) = &self.0 {
+                    f.write_str(" ")?;
+                    v.fmt(f)
+                } else {
+                    Ok(())
+                }
+            }
+        }
+        let space_solver = OptArg(solver.as_ref());
         let smtbmc_options = smtbmc_extra_args.join(" ");
         let top_module = &output.verilog.firrtl.top_module;
         let mut retval = format!(
@@ -488,7 +500,7 @@ impl FormalArgs {
             wait on\n\
             \n\
             [engines]\n\
-            smtbmc {solver} -- -- {smtbmc_options}\n\
+            smtbmc{space_solver} -- -- {smtbmc_options}\n\
             \n\
             [script]\n"
         );

crates/fayalite/src/testing.rs

@@ -115,8 +115,6 @@ pub fn assert_formal<M>(
     args.verilog.debug = true;
     args.mode = mode;
     args.depth = depth;
-    if let Some(solver) = solver {
+    args.solver = solver.map(String::from);
-        args.solver = solver.into();
-    }
     args.run(module).expect("testing::assert_formal() failed");
 }