diff options
| author | François Bobot <francois@bobot.eu> | 2012-04-06 22:51:27 +0000 |
|---|---|---|
| committer | François Bobot <francois@bobot.eu> | 2012-04-06 22:51:27 +0000 |
| commit | 889853e225687dfef36b15ca1dccf74682e0fd66 (patch) | |
| tree | 598f1960f24db5ded582a14efec49c5aeb9488ac /test/regress | |
| parent | 7237456b4e2e5a119feacf98f52ec9e55d7a62a5 (diff) | |
* Smt2 printer for datatypes
* Fix DefineFunctionCommand when a constant is defined
Diffstat (limited to 'test/regress')
| -rwxr-xr-x | test/regress/run_regression | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index 81570e817..587d3cdda 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -13,7 +13,7 @@ prog=`basename "$0"` if [ $# -lt 2 -o $# -gt 3 ]; then - echo "usage: $prog cvc4-binary [ --proof | --dump ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]" >&2 + echo "usage: $prog [ --proof | --dump ] cvc4-binary [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]" >&2 exit 1 fi |