diff --git a/.gitignore b/.gitignore
index a6305dc..28597c5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,9 +1,11 @@
+test/
+results/
 docs/
 benchmarks/
 temp/
 build/
 compile_commands.json
 out/
 include/bbdd/
 *.csv
 trace.vcd
diff --git a/test/run_iscas85.sh b/test/run_iscas85.sh
deleted file mode 100755
index 3c7e0f7..0000000
--- a/test/run_iscas85.sh
+++ /dev/null
@@ -1,198 +0,0 @@
-#!/bin/bash
-# Non-interactive ISCAS85 regression runner for the DD synthesis passes.
-#
-# Renders one of the yosys script templates for every ISCAS85 circuit, runs it
-# with the SAT equivalence check enabled, and reports for each circuit whether
-# the optimised netlist was proven equivalent to the golden one.
-#
-# Usage: test/run_iscas85.sh [-n MAX_INPUTS] [-t TIMEOUT] [-o OUT_DIR]
-#                           [-s SCRIPT] [-k] [circuit ...]
-#
-#   -n  max inputs per partition block, forwarded to the converter as -n
-#       (0 or unset = no partitioning, i.e. the original behaviour)
-#   -t  timeout for the converter call itself       (default 2m)
-#   -T  timeout for the whole yosys run             (default 10m)
-#   -o  output directory                            (default out/iscas85)
-#   -s  yosys script template   (default yosys/bbdd_synth_muxxor.ys)
-#   -k  keep the rendered .ys and intermediate blif files
-#
-# With no circuit names all 11 ISCAS85 benchmarks are run.
-
-set -u
-
-BENCH_DIR="benchmarks/ISCAS85"
-SCRIPT="yosys/bbdd_synth_muxxor.ys"
-OUT_DIR="out/iscas85"
-TEMP_DIR="temp"
-LIBERTY_FILE="liberty/nem_thesis.lib"
-TECHMAP_BBDD="yosys/techmap_bbdd.v"
-TIMEOUT="2m"
-YOSYS_TIMEOUT="10m"
-MAX_INPUTS=0
-KEEP=false
-
-while getopts "n:t:T:o:s:k" opt; do
-  case "$opt" in
-    n) MAX_INPUTS="$OPTARG" ;;
-    t) TIMEOUT="$OPTARG" ;;
-    T) YOSYS_TIMEOUT="$OPTARG" ;;
-    o) OUT_DIR="$OPTARG" ;;
-    s) SCRIPT="$OPTARG" ;;
-    k) KEEP=true ;;
-    *) sed -n '2,20p' "$0"; exit 1 ;;
-  esac
-done
-shift $((OPTIND - 1))
-
-if [ ! -f "$SCRIPT" ]; then
-  echo "[ERROR] script template not found: $SCRIPT" >&2
-  exit 1
-fi
-if [ ! -x ./build/src/convert_bbdd ]; then
-  echo "[ERROR] ./build/src/convert_bbdd missing - build first:" >&2
-  echo "        mkdir -p build && cd build && cmake .. && make" >&2
-  exit 1
-fi
-
-# Circuits: either those named on the command line, or all of ISCAS85.
-if [ $# -gt 0 ]; then
-  CIRCUITS=("$@")
-else
-  CIRCUITS=()
-  for d in "$BENCH_DIR"/*/; do
-    CIRCUITS+=("$(basename "${d%/}")")
-  done
-fi
-
-# yosys 0.40 added `flatten -noscopeinfo`; on older yosys the flag is a hard
-# error, and plain `flatten` is equivalent there because no $scopeinfo cells
-# are ever produced. Detect once and patch the rendered script if needed.
-STRIP_NOSCOPEINFO=false
-if ! yosys -qp "help flatten" 2>/dev/null | grep -q -- "-noscopeinfo"; then
-  STRIP_NOSCOPEINFO=true
-  echo "[INFO] yosys $(yosys -V 2>/dev/null | awk '{print $2}') has no 'flatten -noscopeinfo'; stripping the flag"
-fi
-
-safe_path() { printf '%s\n' "$1" | sed 's/[&/\]/\\&/g'; }
-
-# Converter options are injected through {{CONV_FLAGS}}. Only the bbdd template
-# carries that placeholder; convert_bdd still takes no options at all, so -n
-# would be dropped without a word here.
-if ! grep -q "{{CONV_FLAGS}}" "$SCRIPT" && [ "$MAX_INPUTS" -gt 0 ] 2>/dev/null; then
-  echo "[ERROR] $SCRIPT has no {{CONV_FLAGS}} placeholder; -n cannot be forwarded" >&2
-  exit 1
-fi
-
-mkdir -p "$TEMP_DIR" "$OUT_DIR"
-
-RESULTS=()
-
-for name in "${CIRCUITS[@]}"; do
-  src="$BENCH_DIR/$name/$name.v"
-  if [ ! -f "$src" ]; then
-    echo "[WARN] no such benchmark: $src" >&2
-    continue
-  fi
-
-  mkdir -p "$OUT_DIR/$name"
-  rendered="$TEMP_DIR/${name}_synth.ys"
-  log="$OUT_DIR/$name/yosys.log"
-
-  conv_flags="-t 300000"
-  if [ "$MAX_INPUTS" -gt 0 ] 2>/dev/null; then
-    conv_flags="$conv_flags -n $MAX_INPUTS"
-  fi
-
-  sed -e "s/{{VERILOG_FILE}}/$(safe_path "$src")/g" \
-      -e "s/{{TEMP_DIR}}/$(safe_path "$TEMP_DIR")/g" \
-      -e "s/{{TOP_MODULE}}/$name/g" \
-      -e "s/{{BASE_NAME}}/$name/g" \
-      -e "s/{{TECHMAP_BBDD}}/$(safe_path "$TECHMAP_BBDD")/g" \
-      -e "s/{{LIBERTY_FILE}}/$(safe_path "$LIBERTY_FILE")/g" \
-      -e "s/{{OUT_DIR}}/$(safe_path "$OUT_DIR")/g" \
-      -e "s/{{TIMEOUT}}/$TIMEOUT/g" \
-      -e "s/{{SAT}}//g" \
-      -e "s/{{CONV_FLAGS}}/$(safe_path "$conv_flags")/g" \
-      "$SCRIPT" > "$rendered"
-
-  if $STRIP_NOSCOPEINFO; then
-    sed -i 's/flatten -noscopeinfo/flatten/' "$rendered"
-  fi
-
-  # yosys -l only captures what yosys itself prints; the converter is spawned
-  # through `exec` and writes to the inherited stderr, so its diagnostics
-  # (e.g. "Unique Table is full") only show up in the combined stdio stream.
-  stdio="$OUT_DIR/$name/stdio.log"
-
-  printf '%-8s ' "$name"
-  start=$(date +%s.%N)
-  timeout "$YOSYS_TIMEOUT" yosys -ql "$log" "$rendered" > "$stdio" 2>&1
-  rc=$?
-  end=$(date +%s.%N)
-  elapsed=$(awk -v a="$start" -v b="$end" 'BEGIN{printf "%.1f", b-a}')
-
-  # Classify. The SAT step is `sat -prove-asserts -tempinduct ... equal`.
-  # With -tempinduct yosys reports "Induction step proven: SUCCESS!"; without
-  # it, "SAT proof finished - no model found: SUCCESS!". Accept either.
-  if [ $rc -eq 124 ]; then
-    verdict="TIMEOUT(yosys)"
-  elif grep -qE "Induction step failed|model found: FAIL|Assert failed|induction length [0-9]+ failed" "$log" "$stdio" 2>/dev/null; then
-    verdict="FAIL"
-  elif grep -qE "Induction step proven: SUCCESS|no model found: SUCCESS" "$log" "$stdio" 2>/dev/null; then
-    verdict="PASS"
-  elif grep -q "Unique Table is full" "$log" "$stdio" 2>/dev/null; then
-    # the converter exhausted its hash table: a capacity problem, not a
-    # timeout, and it aborts within seconds rather than running long
-    verdict="TABLE-FULL"
-  elif grep -qE "Assertion .* failed|Segmentation fault" "$log" "$stdio" 2>/dev/null; then
-    verdict="ASSERT"
-  elif grep -qE "did not finish in time|Command failed: timeout|ERROR: Can't open input file" "$log" "$stdio" 2>/dev/null; then
-    verdict="TIMEOUT(conv)"
-  elif [ $rc -ne 0 ]; then
-    verdict="ERROR($rc)"
-  else
-    verdict="NO-PROOF"
-  fi
-
-  # Stats straight out of the blif the flow already writes.
-  blif="$TEMP_DIR/$name.blif"
-  pi=$(awk '/^\.inputs/{print NF-1; exit}' "$blif" 2>/dev/null)
-  po=$(awk '/^\.outputs/{print NF-1; exit}' "$blif" 2>/dev/null)
-  gold=$(python3 -c "
-import json,sys
-try:
-  d=json.load(open('$OUT_DIR/$name/${name}_golden.json'))
-  m=list(d['modules'].values())[0]
-  print(sum(m['num_cells_by_type'].values()))
-except Exception: print('-')" 2>/dev/null)
-  opt=$(python3 -c "
-import json,sys
-try:
-  d=json.load(open('$OUT_DIR/$name/${name}_bbdd.json'))
-  m=list(d['modules'].values())[0]
-  print(sum(m['num_cells_by_type'].values()))
-except Exception: print('-')" 2>/dev/null)
-
-  echo "PI=${pi:--} PO=${po:--} gates:${gold:--}->${opt:--} ${elapsed}s  $verdict"
-  RESULTS+=("$name|${pi:--}|${po:--}|${gold:--}|${opt:--}|${elapsed}|$verdict")
-
-  if ! $KEEP; then
-    rm -f "$rendered" "$TEMP_DIR/${name}_bbdd.blif" "$TEMP_DIR/${name}_bdd.blif"
-  fi
-done
-
-n_label=$([ "$MAX_INPUTS" -gt 0 ] 2>/dev/null && echo "$MAX_INPUTS" || echo "off")
-
-echo
-echo "| Circuit | PIs | POs | n | Gates (golden) | Gates (bbdd) | Runtime | SAT equivalence |"
-echo "|---|---|---|---|---|---|---|---|"
-for r in "${RESULTS[@]}"; do
-  IFS='|' read -r c pi po g o t v <<< "$r"
-  echo "| $c | $pi | $po | $n_label | $g | $o | ${t}s | $v |"
-done
-
-# exit non-zero if anything actually miscompiled (timeouts are not failures here)
-for r in "${RESULTS[@]}"; do
-  case "$r" in *"|FAIL") exit 1 ;; esac
-done
-exit 0