$ z3 --version
Z3 version 4.13.3 - 64 bit
$ z3 no_regress_of_giving.smt2
check 1: OP-001 + two-step giving (c gives b, b gives a) (expect unsat)
unsat
check 2: two-step giving without OP-001 (expect sat: OP-001 is needed)
sat
check 3: OP-001 + base t gives existence to a, b, c; proximate chain c -> b -> a; all exist (expect sat)
sat
exit code: 0
$ shasum -a 256 no_regress_of_giving.smt2
312ff850312fb8f307a4ac8837a41254159bdde2cd26e70587d52f40644f21df  no_regress_of_giving.smt2
checked: 2026-09-29