Fixes after rebasing

src/driver.rs

@@ -683,10 +683,10 @@ impl<'ctx> SmtVcUnit<'ctx> {
         let _entered = span.enter();
 
         let mut prover = mk_valid_query_prover(limits_ref, ctx, translate, &self.vc);
-        if options.force_ematching {
+        if options.opt_options.force_ematching {
             prover.enforce_ematching();
         }
-        if let Some(seed) = options.z3_seed {
+        if let Some(seed) = options.debug_options.z3_seed {
             prover.seed(seed);
         }
 

src/main.rs

@@ -249,7 +249,7 @@ pub struct DebugOptions {
     pub z3_trace: bool,
 
     /// An explicit seed used by Z3 for the final SAT check.
-    #[structopt(long)]
+    #[arg(long)]
     pub z3_seed: Option<u32>,
 }
 
@@ -721,8 +721,8 @@ fn verify_files_main(
             &ctx,
             &tcx,
             SmtCtxOptions {
-                use_limited_functions: options.limited_functions,
-                lit_wrap: options.lit_wrap,
+                use_limited_functions: options.opt_options.limited_functions,
+                lit_wrap: options.opt_options.lit_wrap,
             },
         );
         let mut translate = TranslateExprs::new(&smt_ctx);

src/slicing/transform_test.rs

@@ -16,7 +16,7 @@ use crate::{
     tyctx::TyCtx,
     vc::vcgen::Vcgen,
 };
-
+use crate::smt::SmtCtxOptions;
 use super::{
     selection::SliceSelection,
     transform::{SliceStmt, SliceStmts, StmtSliceVisitor},
@@ -121,7 +121,7 @@ fn prove_equiv(
         stmt2_vc.clone(),
     );
     let ctx = z3::Context::new(&z3::Config::new());
-    let smt_ctx = SmtCtx::new(&ctx, tcx);
+    let smt_ctx = SmtCtx::new(&ctx, tcx, SmtCtxOptions::default());
     let mut translate = TranslateExprs::new(&smt_ctx);
     let eq_expr_z3 = translate.t_bool(&eq_expr);
     let mut prover = Prover::new(&ctx);

src/smt/limited.rs

@@ -8,6 +8,7 @@
 //! For this to work the SMT solver is not allowed to synthesis fuel values itself.
 //! Therefore, MBQI must be disabled.
 
+use std::collections::HashSet;
 use crate::ast::visit::{walk_expr, VisitorMut};
 use crate::ast::{
     Expr, ExprBuilder, ExprData, ExprKind, FuncDecl, Ident, PointerHashShared, QuantVar,
@@ -263,7 +264,7 @@ pub fn return_value_invariant<'smt, 'ctx>(
 type HashExpr = PointerHashShared<ExprData>;
 
 #[derive(Default)]
-pub struct ConstantExprs(IndexSet<HashExpr>);
+pub struct ConstantExprs(HashSet<HashExpr>);
 
 impl ConstantExprs {
     pub fn is_constant(&self, expr: &Expr) -> bool {

src/smt/translate_exprs.rs

@@ -1,9 +1,9 @@
 //! Translation of Caesar expressions to Z3 expressions.
 
 use itertools::Itertools;
-use once_cell::unsync::OnceCell;
 use ref_cast::RefCast;
 use std::{collections::HashMap, convert::TryFrom, vec};
+use std::cell::OnceCell;
 use z3::{
     ast::{Ast, Bool, Dynamic, Int, Real},
     Pattern,
@@ -813,7 +813,11 @@ impl<'ctx> QuantifiedFuel<'ctx> {
     pub fn new(value: Option<ScopeSymbolic<'ctx>>) -> Self {
         Self {
             lazy_fuel: match value {
-                Some(s) => OnceCell::with_value(s),
+                Some(s) => {
+                    let cell = OnceCell::new();
+                    cell.set(s).unwrap_or_else(|_| unreachable!("Cell was newly constructed"));
+                    cell
+                },
                 None => OnceCell::new(),
             },
         }