1180 lines
22 KiB
Plaintext
1180 lines
22 KiB
Plaintext
exploit brake_pads(a)=
|
|
preconditions:
|
|
quality:a,brake_months>=6;
|
|
quality:a,brake_vio=false;
|
|
postconditions:
|
|
update quality:a,brake_vio=true;
|
|
update quality:a,compliance_vio=true;
|
|
.
|
|
|
|
exploit exhaust_pipes(a)=
|
|
preconditions:
|
|
quality:a,exhaust_months>=12;
|
|
quality:a,exhaust_vio=false;
|
|
postconditions:
|
|
update quality:a,compliance_vio=true;
|
|
update quality:a,exhaust_vio=true;
|
|
.
|
|
|
|
exploit ac_filter(a)=
|
|
preconditions:
|
|
quality:a,ac_odometer>=12000;
|
|
quality:a,ac_vio=false;
|
|
postconditions:
|
|
insert quality:a,is_critical=true;
|
|
update quality:a,compliance_vio=true;
|
|
update quality:a,ac_vio=true;
|
|
.
|
|
|
|
exploit vacuum_pump(a)=
|
|
preconditions:
|
|
quality:a,vacuum_odometer>=120000;
|
|
quality:a,engine=diesel;
|
|
quality:a,vacuum_vio=false;
|
|
postconditions:
|
|
insert quality:a,is_critical=true;
|
|
update quality:a,compliance_vio=true;
|
|
update quality:a,vacuum_vio=true;
|
|
.
|
|
|
|
|
|
exploit brake_service(a)=
|
|
preconditions:
|
|
quality:a,brake_months>=6;
|
|
quality:a,brake_vio=true;
|
|
postconditions:
|
|
update quality:a,brake_months=0;
|
|
update quality:a,brake_vio=false;
|
|
.
|
|
|
|
|
|
time group exploit time_advance(a)=
|
|
preconditions:
|
|
quality:a,TIME_ADVANCE_STEP<13;
|
|
quality:a,brake_months<6;
|
|
quality:a,brake_vio=false;
|
|
postconditions:
|
|
update quality:a,brake_months+=1;
|
|
update quality:a,vacuum_odometer+=10000;
|
|
update quality:a,ac_odometer+=10000;
|
|
update quality:a,exhaust_months+=1;
|
|
update quality:a,TIME_ADVANCE_STEP+=1;
|
|
.
|
|
|
|
exploit dummy_1(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_2(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_3(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_4(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_5(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_6(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_7(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_8(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_9(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_10(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_11(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_12(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_13(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_14(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_15(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_16(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_17(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_18(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_19(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_20(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_21(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_22(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_23(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_24(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_25(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_26(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_27(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_28(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_29(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_30(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_31(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_32(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_33(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_34(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_35(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_36(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_37(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_38(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_39(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_40(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_41(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_42(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_43(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_44(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_45(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_46(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_47(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_48(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_49(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_50(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_51(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_52(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_53(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_54(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_55(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_56(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_57(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_58(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_59(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_60(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_61(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_62(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_63(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_64(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_65(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_66(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_67(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_68(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_69(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_70(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_71(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_72(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_73(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_74(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_75(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_76(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_77(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_78(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_79(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_80(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_81(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_82(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_83(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_84(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_85(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_86(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_87(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_88(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_89(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_90(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_91(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_92(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_93(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_94(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_95(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_96(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_97(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_98(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_99(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_100(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_101(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_102(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_103(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_104(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_105(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_106(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_107(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_108(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_109(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_110(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_111(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_112(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_113(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_114(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_115(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_116(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_117(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_118(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_119(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_120(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_121(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_122(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_123(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_124(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_125(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_126(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_127(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_128(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_129(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_130(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_131(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_132(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_133(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_134(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_135(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_136(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_137(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_138(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_139(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_140(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_141(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_142(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_143(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_144(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_145(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_146(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_147(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_148(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_149(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_150(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_151(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_152(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_153(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_154(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_155(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_156(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_157(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_158(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_159(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_160(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_161(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_162(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_163(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_164(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_165(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_166(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_167(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_168(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_169(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_170(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_171(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_172(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_173(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_174(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_175(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_176(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_177(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_178(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_179(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_180(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_181(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_182(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_183(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_184(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_185(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|
|
exploit dummy_186(a)=
|
|
preconditions:
|
|
quality:a,can_fly=true;
|
|
postconditions:
|
|
insert quality:a,flying_car=true;
|
|
.
|