SMTLIB output validation suite #1741
Conversation
rafaelsamenezes
force-pushed
the
smtlib-test
branch
from
060a3a8
to
9cf9da0
Compare
| --modes ${modes} | ||
| --file=${test} | ||
| --smt_test | ||
| --smt_solver=z3 |
There was a problem hiding this comment.
This assumes that the executable z3 is installed on the UNIX AND NOT APPLE system. For my PC that's true, but can we expect that for everyone running ctest?
There was a problem hiding this comment.
Oops, I am going to do a proper add_executable call here.
| # NOTE: We can't check for RC as some CORE test cases results in PARSING ERRORS :) | ||
| if TestCase.RUN_ONLY: | ||
| if rc != 0: | ||
| self.fail(f"Wrong output for process. Bombed out with exit code {rc}") |
There was a problem hiding this comment.
What's the problem with the PARSING ERROR tests here? They did exist before, no?
There was a problem hiding this comment.
No problem, I am just not sure what we are verifying at this point. Are we verifying for a successful execution? It can be verification successful, SMTLIB, verification failed, parsing error. We could try to validate every one of them individually, but then we don't know what the original test case wanted.
Thats why I was annoyed that the PARSING ERROR for a limitation is in core. That being said, we could also consider testing whether the frontend can find issues correctly.
So, I preferred to just disable it. RUN_ONLY should check some byproduct of the run, not the run itself.
This allow us to check whether the SMTLIB output is producing valid formulas by checking the produced formulas against Z3. I also removed the --array-flattener flag from the default flags as it was causing some error in ESBMC (I will open an issue later for those).