search

sl-comp / SL-COMP18

Resources for the SL-COMP 2018 edition
3 stars 2 forks source link

Resolve conflicts in variable naming and input keywords for the translator of Songbird #17

Closed ghost closed 6 years ago

ghost commented 6 years ago

Hi,

I notice that some of the test cases use some variables' names and data structures' field names', which happen to be the same as keywords in the input format of our prover Songbird.

For example, the test case dll-sat-06.smt2 in the category qf_shidlia_sat, the data structure is declared as:

(declare-datatypes (
    (Dll_t 0)
    ) (
    ((c_Dll_t (next RefDll_t) (prev RefDll_t) (data Int) ))
    )
)

When being translated into Songbird's format, the field name data in (data Int) is not allowed, since data is a keyword in Songbird's format.

Hence, I created this patch to the translator of Songbird to resolve this naming conflict.

Could you please merge it back into the original repo?

Thank you very much!