I observe that some properties from the contract library are re-proved in every single SMT file, every time. For a simple function, we always see repeated proof of the following number of properties, for example:
__CPROVER_contracts_car_create 3
__CPROVER_contracts_car_set_insert 3
__CPROVER_contracts_is_fresh 6
__CPROVER_contracts_make_invalid_pointer 6
__CPROVER_contracts_obj_set_create_indexed_by_object_id 3
__CPROVER_contracts_write_set_check_assignment 4
They always report “SUCCESS” so why repeat the proof of them every time?
Can these be elimited from the SMT file once and for all?
I observe that some properties from the contract library are re-proved in every single SMT file, every time. For a simple function, we always see repeated proof of the following number of properties, for example:
__CPROVER_contracts_car_create 3
__CPROVER_contracts_car_set_insert 3
__CPROVER_contracts_is_fresh 6
__CPROVER_contracts_make_invalid_pointer 6
__CPROVER_contracts_obj_set_create_indexed_by_object_id 3
__CPROVER_contracts_write_set_check_assignment 4
They always report “SUCCESS” so why repeat the proof of them every time?
Can these be elimited from the SMT file once and for all?