Correctly construct SmtCtx in test

moves-rwth · Nov 5, 2024 · 86bf19f · 86bf19f
1 parent 71a19ac
commit 86bf19f
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/opt/fuzz_test.rs b/src/opt/fuzz_test.rs
@@ -4,6 +4,7 @@ use proptest::{
 };
 use z3rro::prover::{ProveResult, Prover};
 
+use crate::smt::SmtCtxOptions;
 use crate::{
     ast::{
         BinOpKind, DeclKind, DeclRef, Expr, ExprBuilder, ExprData, ExprKind, Ident, LitKind,
@@ -198,7 +199,7 @@ fn prove_equiv(expr: Expr, optimized: Expr, tcx: &TyCtx) -> TestCaseResult {
         optimized.clone(),
     );
     let ctx = z3::Context::new(&z3::Config::new());
-    let smt_ctx = SmtCtx::new(&ctx, tcx, false, false);
+    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);