Change run-regression script to *additionally* run a second test with --check-models...
authorMorgan Deters <mdeters@gmail.com>
Sat, 10 Nov 2012 17:08:54 +0000 (17:08 +0000)
committerMorgan Deters <mdeters@gmail.com>
Sat, 10 Nov 2012 17:08:54 +0000 (17:08 +0000)
commit1161090e572f85d2ed191b66315406daa7ba7527
treeea8751f927a4640bbf91e908953a7e872bc74043
parent3169a068f1a0a6b1f8cc902847d106664d6c0bd9
Change run-regression script to *additionally* run a second test with --check-models *if* the benchmark is sat/invalid (or is incremental, with at least one sat/invalid result).

This increases significantly the time to do a "make regress", as more tests are running.

We need to run both *with* and *without* --check-models, since that option disables certain preprocessing.

To turn off these extra tests during a make regress, you can set CVC4_REGRESSION_ARGS=--no-check-models.

To turn off the extra test for a *particular* regression benchmark, you can put this in the benchmark:

; COMMAND-LINE: --no-check-models

That might be necessary in e.g. nonlinear arithmetic benchmarks.

(this commit was certified error- and warning-free by the test-and-commit script.)
test/regress/run_regression