diff --git a/src/tools/README.md b/src/tools/README.md
new file mode 100644
index 00000000..ce8571b6
--- /dev/null
+++ b/src/tools/README.md
@@ -0,0 +1,13 @@
+
+## ddSMT
+
+to use ddSMT (from https://github.com/ddsmt/ddSMT/issues):
+
+Assuming `bad_file.smt2` is UNSAT but sidekick returns SAT:
+```sh
+ddsmt.py -vv bad_file.smt2 foo.smt2 ./src/tools/ddsmt_driver_unsat.py
+```
+
+Once it's done, `foo.smt2` should contain a minimal problematic file.
+
+
diff --git a/src/tools/ddsmt_driver_sat.py b/src/tools/ddsmt_driver_sat.py
new file mode 100755
index 00000000..0ea73cee
--- /dev/null
+++ b/src/tools/ddsmt_driver_sat.py
@@ -0,0 +1,15 @@
+#!/usr/bin/python
+
+import subprocess, sys
+
+filename: str = sys.argv[1]
+
+z3_out = subprocess.run([b'z3', filename], capture_output=True).stdout
+if b'sat' not in z3_out or b'unsat' in z3_out or b'error' in z3_out:
+    sys.exit(0)
+
+b_out = subprocess.run([b'./mc2', filename], capture_output=True).stdout
+if b_out.startswith(b'Unsat') and b'Error' not in b_out:
+    print('ohno', file=sys.stderr)
+    sys.exit(1)
+
diff --git a/src/tools/ddsmt_driver_unsat.py b/src/tools/ddsmt_driver_unsat.py
new file mode 100755
index 00000000..b51f84b7
--- /dev/null
+++ b/src/tools/ddsmt_driver_unsat.py
@@ -0,0 +1,21 @@
+#!/usr/bin/python
+
+# minimize unsat problem
+
+import subprocess, sys
+
+filename: str = sys.argv[1]
+
+z3_out = subprocess.run([b'z3', filename], capture_output=True).stdout
+if b'unsat' not in z3_out or b'error' in z3_out:
+    print("z3 failed")
+    sys.exit(1)
+
+b_out = subprocess.run([b'./sidekick', filename], capture_output=True).stdout
+if b'Sat' not in b_out or b'Error' in b_out:
+    print('ohno', file=sys.stderr)
+    print(b_out, sys.stderr)
+    sys.exit(2)
+
+sys.exit(0)
+