Unchecked exit

[m-fleury]

Hi all,

The SMT Competition 2023 requires the SMT problems to have an exit call at the end, but dolmen does not check for it. Is there an option to force dolmen to check for exit?

$ ./quick-check.sh non-incremental/QF_BV/20230221-oisc-fleury/SRAI-SAFE-1024-1024.smt2 
::group::Checking "non-incremental/QF_BV/20230221-oisc-fleury/SRAI-SAFE-1024-1024.smt2"
                File: non-incremental/QF_BV/20230221-oisc-fleury/SRAI-SAFE-1024-1024.smt2
       Logic in path: QF_BV
        Type in path: non-incremental
       Logic in file: QF_BV
            Encoding: us-ascii
             SMT-LIB: 2.6
             License: CC
            Category: industrial
::error file=non-incremental/QF_BV/20230221-oisc-fleury/SRAI-SAFE-1024-1024.smt2::No exit command found.
        Type of file: non-incremental

$ dolmen -i smt2 --check-headers=true --header-lang-version=2.6 non-incremental/QF_BV/20230221-oisc-fleury/SRAI-SAFE-1024-1024.smt2

$

[Gbury]

Hi @m-fleury , dolmen currently does not check that there is an exit at the end of a file. I'll work on adding that asap (it's already part of issue #50 )

[m-fleury]

Ah sorry, I missed that it was already tracked. Thank you for your hard work!

[Gbury]

No worries, it's actually useful to know what to prioritize, ^^

[Gbury]

@m-fleury now that #135 has been merged, and as soon as I make the new release, you'll be able to do:

$ dolmen --check-flow=true tests/flow/missing_exit.smt2 
File "tests/flow/missing_exit.smt2", <location missing>:
Error Missing exit statement