Verification programs with ADTs using Shallow Horn Clauses



For understanding the logs of the solver, you can read this note.

True properties as (Proved,DontKnow,Disproved): (108, 35, 0) ------- False properties as (Proved,DontKnow,Disproved): (0, 0, 32)

POSITIVE INSTANCES

Instance name Answer Time (in sec) ICE iterations
append_equal_elt Proved 6.6263 12
append_equal_nat Unknown 60.9847 20
append_length_commutative Unknown 59.3374 30
append_length_leq_elt Proved 0.2817 13
append_length_leq_nat Proved 0.4014 15
append_not_null_cons_elt Proved 0.0318 3
append_not_null_cons_nat Proved 0.0326 3
append_not_null_elt Proved 0.0317 3
append_not_null_nat Proved 0.0560 3
cons_injectivity_1 Proved 0.0076 0
cons_injectivity_2 Proved 0.0163 0
cons_not_null Proved 0.0137 1
delete_one_insert Unknown 60.9614 35
drop_length_minus Unknown 60.8491 23
fst_elist Proved 4.8020 13
fst_elt Proved 0.0315 3
fst_nat Proved 0.0652 5
fst_nlist Proved 12.0884 14
insert_length_eq Proved 0.2804 10
insert_length_leq Proved 0.3378 16
insert_not_nil Proved 0.0405 3
isaplanner_prop10 Proved 0.0992 6
isaplanner_prop11 Proved 0.1642 7
isaplanner_prop13 Unknown 59.6811 13
isaplanner_prop15 Proved 0.1845 11
isaplanner_prop16 Proved 0.1186 5
isaplanner_prop17 Proved 0.0364 4
isaplanner_prop18 Proved 0.1278 10
isaplanner_prop19 Unknown 59.1606 21
isaplanner_prop20 Proved 0.7915 14
isaplanner_prop21 Proved 0.0957 8
isaplanner_prop22 Proved 0.1040 7
isaplanner_prop23 Proved 0.0925 7
isaplanner_prop24 Proved 0.0839 7
isaplanner_prop25 Proved 0.1045 7
isaplanner_prop26 Unknown 60.7338 22
isaplanner_prop27 Unknown 60.0333 15
isaplanner_prop28 Unknown 59.2907 18
isaplanner_prop31 Proved 0.0295 3
isaplanner_prop32 Proved 0.0280 3
isaplanner_prop33 Proved 0.0421 4
isaplanner_prop34 Proved 0.0380 4
isaplanner_prop4 Unknown 60.0587 17
isaplanner_prop40 Proved 0.0243 2
isaplanner_prop42 Proved 0.0766 5
isaplanner_prop44 Unknown 60.0526 23
isaplanner_prop45 Proved 5.8220 15
isaplanner_prop49 Unknown 60.9714 26
isaplanner_prop51 Unknown 60.3970 32
isaplanner_prop54 Unknown 60.8292 18
isaplanner_prop59 Unknown 60.4337 22
isaplanner_prop65 Proved 0.1614 11
isaplanner_prop68 Proved 0.3262 14
isaplanner_prop69 Proved 0.0708 8
isaplanner_prop70 Proved 0.0573 4
isaplanner_prop79 Unknown 60.9892 27
isaplanner_prop80 Unknown 60.9724 29
length_append_le_z Proved 0.0670 5
length_append_to_plus Unknown 60.7654 22
length_cons_le Proved 0.0669 7
length_cons_le_fun_elt Proved 0.1498 10
length_cons_le_fun_nat Proved 0.1643 10
length_cons_le_tsil Proved 0.1058 7
length_cons_s Proved 0.0620 3
length_count Proved 0.2752 12
length_delete_leq Proved 0.1886 12
length_delete_minus_count Unknown 59.4427 31
length_reverse_eq Proved 17.0210 25
length_reverse_eq_nat Proved 26.1636 25
length_reverse_leq_elt Proved 27.5054 30
length_reverse_leq_nat Proved 32.6449 30
length_take_if Proved 0.0680 5
leq_leq_eq Proved 0.0711 6
list_delete_all_count Unknown 59.9072 28
max_nat Proved 0.0658 6
mem_implies_positive_count Proved 1.6710 15
mem_reverse Unknown 60.3884 27
member_equal_ab Proved 0.1716 7
member_equal_nat Unknown 59.5248 19
merge_length_leq Proved 0.3563 13
min_of_plus_and_max Unknown 60.5750 25
mult_leq_not_null Proved 0.0909 8
mult_leq_succ Proved 0.1221 10
nat_double_is_even Proved 0.0773 5
nat_double_is_le Proved 0.0428 5
nat_double_is_zero Proved 0.0203 2
nat_double_is_zero_ite Proved 0.0208 2
not_null_transitive Proved 0.0129 1
plus_commutative Unknown 60.1330 27
plus_even_even Proved 0.2624 12
plus_le Proved 0.2001 11
plus_le_le Proved 0.1600 11
plus_not_zero_implication Proved 0.0388 3
plus_odd_odd_even Proved 0.1275 10
plus_succ_le_1 Proved 0.1242 7
plus_succ_le_2 Proved 0.2208 13
plus_succ_not_zero Proved 0.0498 3
prefix_append Proved 0.2338 9
prefix_count Unknown 60.1710 24
prefix_nil Proved 0.0538 4
reverse_not_null Proved 0.0528 3
sort_append Unknown 60.0541 24
sort_cons Unknown 60.9021 26
sort_length_eq Proved 0.7466 15
sort_reverse Unknown 59.3215 26
swap_swap_eq_elt Proved 0.0433 3
swap_swap_eq_nat Proved 0.0798 5
timbuk_delete_not_member Unknown 60.1737 35
timbuk_equalNat Proved 0.0060 0
timbuk_insertionSort_elt Proved 0.0469 3
timbuk_plus_even Proved 0.3256 12
timbuk_replaceTree Proved 36.3063 16
timbuk_reverse Proved 0.0702 4
timbuk_reverseImplies Proved 0.0750 3
tree_add_not_eq Proved 0.0095 0
tree_depth_le_node Unknown 60.4663 30
tree_depth_leq_size Proved 13.2392 19
tree_flip_heightRB_heightLB Proved 0.1373 10
tree_flip_preserves_depth Unknown 60.0669 19
tree_flip_preserves_member Proved 2.9669 11
tree_flip_preserves_size Unknown 60.2355 25
tree_flip_preserves_subtree Proved 3.4286 13
tree_flip_twice Proved 0.2363 7
tree_heightMIDDLE Proved 1.8176 18
tree_heightRB_node_le Proved 0.0329 3
tree_heightRB_subtree Proved 0.1277 9
tree_height_heightRB Proved 0.2117 15
tree_height_max_node Unknown 60.0435 20
tree_height_node_leq Proved 0.0429 4
tree_height_numnodes_le Unknown 59.6972 22
tree_higher_leq Proved 0.9718 14
tree_injectivity_1 Proved 0.0063 0
tree_member_leq_size Proved 0.7566 10
tree_nat_depth_leq_size Proved 3.0494 18
tree_nat_flip_twice Proved 0.1489 8
tree_shallow_leq Proved 0.5903 8
tree_shallow_max Proved 0.9158 12
tree_shallow_taller_node Proved 1.1675 10
tree_shallow_taller_subtree Proved 0.8285 9
tree_shallower_rec_leq Proved 0.2914 5
tree_shallower_rec_node_le Proved 0.1762 4
tree_size_le_node Unknown 60.9246 22
tree_strict_subtree_trans Proved 0.2664 8

NEGATIVE INSTANCES

Instance name Answer Time (in sec) ICE iterations
append_equal Disproved 0.0396 3
append_length_le Disproved 0.1271 3
cons_is_equal Disproved 0.0118 1
cons_not_null Disproved 0.0370 3
insert_length_eq Disproved 0.0307 3
isaplanner_prop11 Disproved 0.0395 2
length_take Disproved 0.0232 2
list_delete_all_count Disproved 0.0219 2
max_nat Disproved 0.0916 6
member_cons Disproved 0.0472 3
mult_leq Disproved 0.0589 4
nat_double_is_le Disproved 0.0399 3
plus_even_implies Disproved 0.0511 5
plus_le Disproved 0.0383 3
plus_odd_odd Disproved 0.0382 4
prefix_append Disproved 0.6814 11
prefix_count Disproved 0.0918 7
reverse_not_null Disproved 0.1004 3
sort_bug_length_eq Disproved 1.6956 19
successor_is_equal Disproved 0.0114 1
timbuk_deleteBUG Disproved 0.0583 3
timbuk_equal Disproved 0.0120 1
timbuk_reverseBUGimplies Disproved 0.6317 6
tree_depth_le_error Disproved 0.1120 3
tree_depth_max_error Disproved 0.0384 4
tree_depth_subtree_error Disproved 0.0445 4
tree_heightMIDDLE_error Disproved 0.2467 10
tree_height_numnodes_error Disproved 0.1620 5
tree_shallow_leq_error Disproved 0.8172 7
tree_shallow_subtree_error Disproved 0.1794 7
tree_subtree_height_error Disproved 0.1606 7
tree_taller_max Disproved 0.1672 7