Analysis job
clc_sby0c4jh
Updated Aug 16, 2026, 6:41 AM
failed
0feasible paths
17symbolic variables
—exploration complete
5000 mssolver timeout
Error details
The analysis failed during execution.
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 programcountry, tax_notice_status, bank_account_name_matches, id_address_matches, tax_notice_name_matches, bank_account_country, applicant_age, proof_of_address_status, proof_of_address_name_matches, tax_notice_income_eur, id_status, id_name_matches, requested_amount_eur, household_size, bank_statement_status, proof_of_address_country, declared_annual_income_eur
from concolic_core import analyzable, branch
import z3
@analyzable
def evaluate_subsidy_kyc(
applicant_age: z3.ArithRef,
country: z3.ArithRef,
requested_amount_eur: z3.ArithRef,
declared_annual_income_eur: z3.ArithRef,
household_size: z3.ArithRef,
id_status: z3.ArithRef,
id_name_matches: z3.BoolRef,
id_address_matches: z3.BoolRef,
tax_notice_status: z3.ArithRef,
tax_notice_income_eur: z3.ArithRef,
tax_notice_name_matches: z3.BoolRef,
bank_statement_status: z3.ArithRef,
bank_account_name_matches: z3.BoolRef,
bank_account_country: z3.ArithRef,
proof_of_address_status: z3.ArithRef,
proof_of_address_name_matches: z3.BoolRef,
proof_of_address_country: z3.ArithRef,
) -> z3.ArithRef:
if branch(applicant_age < 18):
return 1
if branch(country == 3):
return 2
if branch(requested_amount_eur <= 0):
return 3
if branch(requested_amount_eur > 20000):
return 3
if branch(id_status != 1):
return 4
if branch(id_name_matches == False):
return 4
if branch(id_address_matches == False):
return 4
if branch(tax_notice_status != 1):
return 5
if branch(tax_notice_name_matches == False):
return 5
income_delta = declared_annual_income_eur - tax_notice_income_eur
if branch(income_delta < 0):
income_delta = 0 - income_delta
if branch(income_delta > 2000):
return 6
if branch(bank_statement_status != 1):
return 7
if branch(bank_account_name_matches == False):
return 7
if branch(bank_account_country == 3):
return 7
if branch(proof_of_address_status != 1):
return 8
if branch(proof_of_address_name_matches == False):
return 8
if branch(proof_of_address_country != country):
return 8
income_ceiling = 22000 + household_size * 8000
if branch(declared_annual_income_eur > income_ceiling):
return 9
max_eligible = 5000 + household_size * 1000
if branch(declared_annual_income_eur < 20000):
max_eligible = max_eligible + 3000
if branch(country == 1):
max_eligible = max_eligible + 1000
if branch(max_eligible > 15000):
max_eligible = 15000
if branch(requested_amount_eur < max_eligible):
max_eligible = requested_amount_eur
return 100000 + max_eligible