Analysis job
clc_bzn6ho9n
Updated Aug 16, 2026, 8:14 PM
completed
8feasible paths
7symbolic variables
yesexploration complete
nonesolver timeout
Constraint atlas
Feasible execution paths
Compact path records. Click a row to inspect its concrete execution details.
| Constraint | Result / metric |
|---|---|
(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
(not a!4))) | (/ 6750027.0 25.0)20,514 |
(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
a!4)) | (/ 2700027.0 25.0)20,551 |
(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
a!3)) | (/ 135027.0 25.0)19,009 |
(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
a!2)) | (- (/ 36.0 5.0))17,467 |
(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not within_budget))) | 09,920 |
(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
foreign_supplier
a!1)) | 09,021 |
(and (not (not supplier_approved)) duplicate_recent) | 05,430 |
(and (not supplier_approved)) | 05,379 |
Top 5 metric scorers
Constraint breakdown by variable
Unique path constraints involving each symbolic variable and the results they produce.
| Variable | Unique constraints | Paths | Details |
|---|---|---|---|
| foreign_supplier | 6 | 6 | show constraints(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
(not a!4)))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
a!4))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
a!3))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
a!2))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not within_budget)))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
foreign_supplier
a!1)) |
| within_budget | 5 | 5 | show constraints(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
(not a!4)))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
a!4))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
a!3))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
a!2))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not within_budget))) |
| amount | 6 | 6 | show constraints(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
(not a!4)))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
a!4))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
a!3))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
a!2))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not within_budget)))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
foreign_supplier
a!1)) |
| expedited | 6 | 6 | show constraints(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
(not a!4)))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
a!4))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
a!3))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
a!2))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not within_budget)))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
foreign_supplier
a!1)) |
| tax_exempt | 0 | 0 | show constraints |
| supplier_approved | 8 | 8 | show constraints(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
(not a!4)))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
a!4))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
a!3))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
a!2))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not within_budget)))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
foreign_supplier
a!1))(and (not (not supplier_approved)) duplicate_recent)(and (not supplier_approved)) |
| duplicate_recent | 7 | 7 | show constraints(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
(not a!4)))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0))
(a!4 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 250000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
(not a!3)
a!4))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0))
(a!3 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 50000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
(not a!2)
a!3))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0))
(a!2 (<= (ite expedited (/ (* amount 23.0) 20.0) amount) 5000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not (not within_budget))
a!2))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
(not (and foreign_supplier a!1))
(not within_budget)))(let ((a!1 (> (ite expedited (/ (* amount 23.0) 20.0) amount) 100000.0)))
(and (not (not supplier_approved))
(not duplicate_recent)
foreign_supplier
a!1))(and (not (not supplier_approved)) duplicate_recent) |
Submitted programforeign_supplier, within_budget, amount, expedited, tax_exempt, supplier_approved, duplicate_recent
import z3
from concolic_core import analyzable, branch
@analyzable
def verify_purchase_order(
amount: z3.ArithRef,
supplier_approved: z3.BoolRef,
duplicate_recent: z3.BoolRef,
expedited: z3.BoolRef,
foreign_supplier: z3.BoolRef,
tax_exempt: z3.BoolRef,
within_budget: z3.BoolRef,
) -> z3.ArithRef:
effective = z3.If(expedited, amount * 23 / 20, amount)
if branch(z3.Not(supplier_approved)):
return 0
if branch(duplicate_recent):
return 0
if branch(z3.And(foreign_supplier, effective > 100000)):
return 0
if branch(z3.Not(within_budget)):
return 0
if branch(effective <= 5000):
level = 1
elif branch(effective <= 50000):
level = 2
elif branch(effective <= 250000):
level = 3
else:
level = 4
tax = z3.If(tax_exempt, 0, effective * 2 / 25)
return effective + tax