rac prover should be executed on a task before transformation compute
The RAC prover is executed on the task obtained after compute_in_goal
, this is not good since for example definition like BV32.sle
are expanded, whereas the prover has a mapping for it in the driver