From 59f89ac660e0b8e914fffe619ab66c353d5fe1ee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cornell.edu>
Date: Mon, 2 Dec 2024 14:06:43 -0500
Subject: [PATCH] update bitwuzla flags and fix bug in unroll function

---
 src/mc/smt.rs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/mc/smt.rs b/src/mc/smt.rs
index a5b919b..52428bd 100644
--- a/src/mc/smt.rs
+++ b/src/mc/smt.rs
@@ -24,7 +24,9 @@ pub struct SmtSolverCmd {
 
 pub const BITWUZLA_CMD: SmtSolverCmd = SmtSolverCmd {
     name: "bitwuzla",
-    args: &["--smt2", "--incremental"],
+    // args: &["--smt2", "--incremental"],
+    // TODO: arguments depend on the version of bitwuzla!
+    args: &[],
     supports_uf: false,
     supports_check_assuming: true,
 };
@@ -532,7 +534,7 @@ impl TransitionSystemEncoding for UnrollSmtEncoding {
 
         // define next state signals for previous state
         self.define_signals(ctx, smt_ctx, prev_step, &|info: &SmtSignalInfo| {
-            info.uses.next > 0 && !info.uses.other > 0 && !info.is_input
+            info.uses.next > 0 && info.uses.other == 0 && !info.is_input
         })?;
 
         // define next state