I am trying to analyze a C program with CBMC but the properties I want to check are written in SMTLIB2. I would prefer to use them as they are within statements __CPROVER_assert(...) than having to translate them to the native, more operational language, using __CPROVER_forall/exists.
Does anyone knows if this is possible when using SMT Solvers as the backend?
I would not find any documentation on this yet it seems to be a valuable pro from using SMT Solvers as backend.