Support for arithmetic Integers is not yet implemented in incremental smt2 decision procedure
esteffin opened this issue · 0 comments
esteffin commented
Support for arithmetic Integers (__CPROVER_Integer
) is not yet implemented in incremental smt2 decision procedure.
This causes a failure with invariant in convert_type_to_smt_sort
about unimplemented generation of formulas for type integer
as an example.
This is required for the following test:
cbmc/integer-assignments1/test.desc