Errors when translating linear arithmetic test cases (category qf_shidlia_entl)

[ghost]

Hi,

I encountered many errors when translating the test cases in the category qf_shidlia_entl. Could you advise how can we handle this issue, since the deadline for prover submission is close

Here are some errors messages:

trungtq@leo /media/trungtq/sda2/Workspace/tools/SL-COMP18-tddsg/tools/slcomp18tools $ ./do-tosolver.sh songbird ../../bench/qf_shidlia_entl/dll_len_append_tail_entails_dllnull.sb.smt2
* File ../../bench/qf_shidlia_entl/dll_len_append_tail_entails_dllnull.sb.smt2
** translate to input format of SL-COMP'14
Warning in Sep::Pp_slcomp14::visit(): Ignore 'set-logic', fix 'QF_S'.
Warning in Sep::Pp_slcomp14::visit(): Ignored DeclareHeap.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
** translate to input format of solver songbird
smtlib2sl: Parse input file
Error of level 1 in sl_mk_minus: bad number (1) of arguments, expected (= 2).
Error of level 1 in sl_mk_minus: bad number (1) of arguments, expected (= 2).
Error of level 1 in sl_mk_minus: bad number (1) of arguments, expected (= 2).
Warning in sl_var_type: look outside vector size.
Error of level 1 in Predicate call to : dll.
Error of level 1 in Bad (last) parameters.: .
Error of level 1 in sl_mk_minus: bad number (1) of arguments, expected (= 2).
Error of level 1 in sl_mk_minus: bad number (1) of arguments, expected (= 2).
Error of level 1 in sl_mk_minus: bad number (1) of arguments, expected (= 2).
Warning in sl_var_type: look outside vector size.
Error of level 1 in Predicate call to : dllnull.
Error of level 1 in Bad (last) parameters.: .
Error of level 0 in sl_check: stop check because of parsing error.

trungtq@leo /media/trungtq/sda2/Workspace/tools/SL-COMP18-tddsg/tools/slcomp18tools $ ./do-tosolver.sh songbird ../../bench/qf_shidlia_entl/dll_len_entails_ls_len_num-1.sb.smt2
* File ../../bench/qf_shidlia_entl/dll_len_entails_ls_len_num-1.sb.smt2
** translate to input format of SL-COMP'14
Warning in Sep::Pp_slcomp14::visit(): Ignore 'set-logic', fix 'QF_S'.
Warning in Sep::Pp_slcomp14::visit(): Ignored DeclareHeap.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
Warning in Sep::Pp_slcomp14::visit(): Ignored numeral.
** translate to input format of solver songbird
smtlib2sl: Parse input file
Error of level 1 in sl_mk_minus: bad number (1) of arguments, expected (= 2).
Error of level 1 in sl_mk_minus: bad number (1) of arguments, expected (= 2).
Error of level 1 in sl_mk_minus: bad number (1) of arguments, expected (= 2).
Warning in sl_var_type: look outside vector size.
Error of level 1 in Predicate call to : dll.
Error of level 1 in Bad (last) parameters.: .
Error of level 1 in sl_mk_minus: bad number (1) of arguments, expected (= 2).
Error of level 1 in sl_mk_minus: bad number (1) of arguments, expected (= 2).
Warning in sl_var_type: look outside vector size.
Error of level 1 in Predicate call to : ls.
Error of level 1 in Bad (last) parameters.: .
Error of level 0 in sl_check: stop check because of parsing error.

Thanks!

[slcomp]

Because SL-COMP'14 format did not support integers, I've fixed to binary te parity of arithmetic terms. The examples coming from Songbird use both unary and binary versions of these operators (+ or -). In SMT-LIB v2.16, unary '-' is allowed, but not unary '+'. For readability, please use binary '-' when possible. For example, instead of '(+ ?l (- 1))' use '(- ?l 1)'.

[slcomp]

A more important limitation now is that arguments of a predicate call (in SL-COMP'14) may be only variables. Therefore the bench using integers or terms in predicate calls are rejected. I'm trying now to fix this problem in the translation from SL-COMP'18 format to SL-COMP'14 format.

[slcomp]

I've fixed all the problems in this benchmark such that they can be translated into SL-COMP'14 format. Please check that Sleek and Snowbird accepts the input in SL-COMP'14 format.