Supporting logic functions and predicates would be a useful addition. They are often used in specifications. Simple examples: https://github.com/rse-verification/auto-deduct-toolchain/blob/autodeduct-support-microtests/autodeduct-support/micro-tests/helper_inference/contract_predicate_helper.c https://github.com/rse-verification/auto-deduct-toolchain/blob/autodeduct-support-microtests/autodeduct-support/micro-tests/helper_inference/contract_logic_function_helper.c
Supporting logic functions and predicates would be a useful addition. They are often used in specifications. Simple examples:
https://github.com/rse-verification/auto-deduct-toolchain/blob/autodeduct-support-microtests/autodeduct-support/micro-tests/helper_inference/contract_predicate_helper.c
https://github.com/rse-verification/auto-deduct-toolchain/blob/autodeduct-support-microtests/autodeduct-support/micro-tests/helper_inference/contract_logic_function_helper.c