Analysis job
clc_rf0xbk3l
Updated Aug 16, 2026, 8:13 PM
failed
4feasible paths
7symbolic variables
—exploration complete
nonesolver timeout
Error details
Float types are not supported. Use Decimal types instead.
Constraint atlas
Feasible execution paths
Compact path records. Click a row to inspect its concrete execution details.
| Constraint | Result / metric |
|---|---|
(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0)))
(a!4 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
a!4)) | (/ 6750027.0 25.0)15,634 |
(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0))) | (/ 2700027.0 25.0)15,671 |
(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0))) | (/ 135027.0 25.0)14,129 |
(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))) | (- (/ 207.0 50.0))12,587 |
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 | 4 | 4 | show constraints(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0)))
(a!4 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
a!4))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0)))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0)))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))) |
| within_budget | 4 | 4 | show constraints(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0)))
(a!4 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
a!4))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0)))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0)))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))) |
| amount | 4 | 4 | show constraints(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0)))
(a!4 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
a!4))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0)))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0)))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))) |
| expedited | 4 | 4 | show constraints(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0)))
(a!4 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
a!4))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0)))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0)))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))) |
| tax_exempt | 0 | 0 | show constraints |
| supplier_approved | 4 | 4 | show constraints(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0)))
(a!4 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
a!4))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0)))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0)))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))) |
| duplicate_recent | 4 | 4 | show constraints(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0)))
(a!4 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
a!4))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0)))
(a!3 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
a!3
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 250000.0)))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0)))
(a!2 (not (<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
a!2
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 50000.0)))(let ((a!1 (and foreign_supplier
(> (ite expedited (* amount (/ 23.0 20.0)) amount) 100000.0))))
(and (not (not supplier_approved))
(not duplicate_recent)
(not a!1)
(not (not within_budget))
(<= (ite expedited (* amount (/ 23.0 20.0)) amount) 5000.0))) |
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 * 1.15, amount)
if branch(z3.Not(supplier_approved)):
return 0.0
if branch(duplicate_recent):
return 0.0
if branch(z3.And(foreign_supplier, effective > 100000)):
return 0.0
if branch(z3.Not(within_budget)):
return 0.0
if branch(effective <= 5000):
level = 1
elif branch(effective <= 50000):
level = 2
elif branch(effective <= 250000):
level = 3
else:
level = 4
tax_rate = z3.If(tax_exempt, 0.0, 0.08)
return effective * (1.0 + tax_rate)