Mentions légales du service

Skip to content

Fix CVC4 counterexample regex

Benedikt Becker requested to merge fix-cvc4-ce-regex into master

Sometimes CVC4 prover models are separated by unknown (RESOURCEOUT) and not unknown, for example in SPARK's test N121-026__nonlinear and many others. This is currently not detected as a separator for models and the trailing model triggers unknown (RESOURCEOUT) in Smtv2_model_parser.

This PR simplifies the steplimit regex in a298d6ed, and fixes a couple of loosely related issues.

Merge request reports