From b1dc7a21ddbe5b44a6a34710be1fecb017b55aeb Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Tue, 12 Nov 2024 16:16:29 -0800
Subject: [PATCH] add solver variants: bitwuzla-abstraction and
 cvc5-int-blasting

---
 src/jsi/config/solvers.json | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/jsi/config/solvers.json b/src/jsi/config/solvers.json
index 82f2efb..f6fec56 100644
--- a/src/jsi/config/solvers.json
+++ b/src/jsi/config/solvers.json
@@ -4,7 +4,11 @@
         "model": "--produce-models",
         "args": [],
         "meta": "only supports model generation if smt file includes (get-model)"
-
+    },
+    "bitwuzla-abstraction": {
+        "executable": "bitwuzla",
+        "model": "--produce-models",
+        "args": ["--abstraction"]
     },
     "boolector": {
         "executable": "boolector",
@@ -21,6 +25,11 @@
         "model": "--produce-models",
         "args": []
     },
+    "cvc5-int-blasting": {
+        "executable": "cvc5",
+        "model": "--produce-models",
+        "args": ["--solve-bv-as-int=iand", "--iand-mode=bitwise"]
+    },
     "stp": {
         "executable": "stp",
         "model": "--print-counterex",