#!/usr/bin/env python3
"""Check both SMT-LIB artifacts with the actual Z3 solver."""
import pathlib
import re
import shutil
import subprocess
import sys

root = pathlib.Path(__file__).resolve().parent
z3 = shutil.which("z3")
if z3 is None:
    sys.exit("Z3 was not found. Follow the setup steps in README.txt.")
for name, expected in [("correct", "unsat"), ("buggy", "sat")]:
    result = subprocess.run([z3, str(root / f"{name}.smt2")], capture_output=True, text=True, timeout=15)
    lines = result.stdout.strip().splitlines()
    if result.returncode != 0 or not lines or lines[0] != expected or "error" in result.stdout.lower():
        sys.exit(f"FAIL {name}: expected {expected}; got {result.stdout!r} {result.stderr!r}")
    print(f"PASS {name} rule: {expected}")
    if name == "buggy":
        values = {key: int(value) for key, value in re.findall(r"\((spent|amount|limit)\s+([0-9]+)\)", result.stdout)}
        if set(values) != {"spent", "amount", "limit"}:
            sys.exit("FAIL: could not read the solver's counterexample")
        spent, amount, limit = (values[key] for key in ("spent", "amount", "limit"))
        if not (0 <= spent <= limit and amount > 0 and spent + amount == limit):
            sys.exit("FAIL: the returned model is not a valid boundary counterexample")
        print(f"Counterexample: spent={spent}, amount={amount}, limit={limit}")
        print("The contract allows the payment. The buggy rule rejects it.")