PPTransSMT: duplicates axiom names

[VTrelat]

Mostly to @DavidDeharbe:

• Link to the issue: https://github.com/CLEARSY/pptranssmt/blob/09b5a4bcebce292b25c7dfb5cf6e7ce42812fc05/PPTRANSSMT/ppTrans.cpp#L212-L249

• Issue: Function registerIterate from namespace ppTrans generates axioms named iterate_axiom_x with x ranging over {1,2,3,4}. Apparently, this function may be called several times, thus generating duplicate iterate_axiom_x names (even though the formulas differ). This makes the smt solver crash.

• Way to solve it:

  • Remove naming (not the best fix)
  • Add a global counter for the name and increment it each time an axiom is written

[dde-cls]

Example exhibiting the reported defect.

m0-0-0.smt2.txt m0.mch.txt m0.pog.txt

[dde-cls]

Fix proposed in commit aadf983707197db2c8c9e24e96a27d38c0f4885f.

The identifiers for the axioms now include the type of the relations over which the iterate operator is axiomatized.

SMT2 file produced with the proposed fix : m0-0-0.fix.smt2.txt

Note: The TPTP backend does not exhibit this errror.

[dde-cls]

Commit with fix: https://github.com/CLEARSY/pptranssmt/commit/d8c69f837734baefa0bfa9620af715c5b219adf3