From 53ef57d58c0bb2f57d7d0d1d1fada7bf3889e03d Mon Sep 17 00:00:00 2001
From: Landon Taylor <landon@mossbiscuits.com>
Date: Thu, 12 Jun 2025 15:12:31 -0600
Subject: [PATCH] Finish SAT/SMT

---
 bitwuzla.yaml      | 10 ++++++++++
 boolector.yaml     | 14 ++++++++++++++
 cryptominisat.yaml | 12 ++++++++++++
 cvc.yaml           | 45 +++++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 81 insertions(+)
 create mode 100644 bitwuzla.yaml
 create mode 100644 boolector.yaml
 create mode 100644 cryptominisat.yaml
 create mode 100644 cvc.yaml

diff --git a/bitwuzla.yaml b/bitwuzla.yaml
new file mode 100644
index 0000000..f5674d6
--- /dev/null
+++ b/bitwuzla.yaml
@@ -0,0 +1,10 @@
+- key: Niemetz2023
+  author:
+    - Aina Niemetz
+    - Mathias Preiner
+  title: Bitwuzla
+  booktitle: CAV 2023
+  pages: 3-17
+  publisher: Springer
+  year: 2023
+  doi: 10.1007/978-3-031-37703-7_1
\ No newline at end of file
diff --git a/boolector.yaml b/boolector.yaml
new file mode 100644
index 0000000..5552ed7
--- /dev/null
+++ b/boolector.yaml
@@ -0,0 +1,14 @@
+- key: Niemetz2014
+  type: article
+  authors:
+    - Aina Niemetz
+    - Mathias Preiner
+    - Armin Biere
+  title: Boolector 2.0
+  journal: J. Satisf. Boolean Model. Comput.
+  volume: 9
+  number: 1
+  pages: 53-58
+  year: 2014
+  # url: https://doi.org/10.3233/sat190101
+  doi: 10.3233/sat190101
\ No newline at end of file
diff --git a/cryptominisat.yaml b/cryptominisat.yaml
new file mode 100644
index 0000000..67529ea
--- /dev/null
+++ b/cryptominisat.yaml
@@ -0,0 +1,12 @@
+- key: Soos2009
+  title: Extending SAT Solvers to Cryptographic Problems
+  author:
+    - Mate Soos
+    - Karsten Nohl
+    - Claude Castelluccia
+  booktitle: SAT 2009
+  volume: 5584
+  pages: 244-257
+  publisher: Springer
+  year: 2009
+  doi: 10.1007/978-3-642-02777-2_24
\ No newline at end of file
diff --git a/cvc.yaml b/cvc.yaml
new file mode 100644
index 0000000..ddffa35
--- /dev/null
+++ b/cvc.yaml
@@ -0,0 +1,45 @@
+- key: Barbosa2022
+  title: 'cvc5: A Versatile and Industrial-Strength SMT Solver'
+  author:
+    - Barbosa, Haniel
+    - Barrett, Clark W.
+    - Brain, Martin
+    - Kremer, Gereon
+    - Lachnitt, Hanna
+    - Mann, Makai
+    - Mohamed, Abdalrhman
+    - Mohamed, Mudathir
+    - Niemetz, Aina
+    - Nötzli, Andres
+    - Ozdemir, Alex
+    - Preiner, Mathias
+    - Reynolds, Andrew
+    - Sheng, Ying
+    - Tinelli, Cesare
+    - Zohar, Yoni
+  year: 2022
+  booktitle: TACAS 2022
+  pages: 415-442
+  publisher: Springer
+  doi: 10.1007/978-3-030-99524-9_24
+
+
+- key: Barrett2011
+  title: 'CVC4'
+  author:
+    - Barrett, Clark W.
+    - Conway, Christopher L.
+    - Deters, Morgan
+    - Hadarean, Liana
+    - Jovanovic, Dejan
+    - King, Tim
+    - Reynolds, Andrew
+    - Tinelli, Cesare
+  year: 2011
+  booktitle: 'Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings'
+  series: Lecture Notes in Computer Science
+  volume: 6806
+  pages: 171-177
+  publisher: Springer
+  doi: 10.1007/978-3-642-22110-1_14
+  url: https://doi.org/10.1007/978-3-642-22110-1_14
\ No newline at end of file