sl-comp / SL-COMP18

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

Error when translating the example qf_shid_entl/dll-vc17.smt2 #21

Closed ghost closed 6 years ago

ghost commented 6 years ago

I think the lines 67, 68 of this test case should be deleted.

            (distinct x_emp z_emp)
            (distinct y_emp z_emp)

Here is the error that I encountered.

* File ../../bench/qf_shid_entl/dll-vc17.smt2
** translate to input format of SL-COMP'14
SmtExecution::checkSortedness(): Well-sortedness errors when checking file '../../bench/qf_shid_entl/dll-vc17.smt2'

-------------------------------------------------
In file '../../bench/qf_shid_entl/dll-vc17.smt2':
-------------------------------------------------
66:20 - 66:24   z_emp
    No possible sorts for constant 'z_emp'.

63:1 - 76:1   (assert (and (distinct x_emp w_emp) (distinct x_emp z_emp) (distinct y_emp z_emp) (sep (pto x_emp (c[...]
    Assertion term '(and (distinct x_emp w_emp) (distinct x_emp z_emp)[...]' (64:3 - 74:3) is not well-sorted.

Error in SmtExecution::translate(): Stopped due to previous errors.
** translate to input format of solver songbird
smtlib2sl: Parse input file
smtlib2sl: *** Translation to songbird
smtlib2sl:  Output file: 
smtlib2sl: dll-vc17.smt2.sl14.sb
Error of level 1 in sl_form_2songbird:: not a PTO, LS, SSEP formula.
smtlib2sl: 
Done
slcomp commented 6 years ago

Indeed, this is fixed now.