Analysis job

clc_ivk9i5u6

Updated Aug 16, 2026, 8:12 PM

failed

0feasible paths

7symbolic variables

—exploration complete

nonesolver timeout

execution error

Error details

NameError: name 'tuple' is not defined

Constraint atlas

Feasible execution paths

Compact path records. Click a row to inspect its concrete execution details.

No paths recorded

The analysis did not produce a feasible execution path.

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,
) -> tuple[z3.ArithRef, z3.ArithRef, z3.ArithRef]:
    effective = z3.If(expedited, amount * 1.15, amount)
    if branch(z3.Not(supplier_approved)):
        return (1, 0, 0.0)
    if branch(duplicate_recent):
        return (2, 0, 0.0)
    if branch(z3.And(foreign_supplier, effective > 100000)):
        return (3, 0, 0.0)
    if branch(z3.Not(within_budget)):
        return (4, 0, 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 (0, level, effective * (1.0 + tax_rate))