diff --git a/rsc/extra/pre-commit--git-hook b/rsc/extra/pre-commit--git-hook index 6528f79d3..675724fc9 100755 --- a/rsc/extra/pre-commit--git-hook +++ b/rsc/extra/pre-commit--git-hook @@ -29,4 +29,4 @@ if [[ $errors -ne 0 ]]; then fi # If there are whitespace errors, print the offending file names and fail. -exec git diff-index --check --cached $against -- +exec git diff-index --check --cached $against -- ':!*.t' ':!*.expected' diff --git a/tests/models/bool/bool1.expected b/tests/models/bool/bool1.expected index e69de29bb..89459232b 100644 --- a/tests/models/bool/bool1.expected +++ b/tests/models/bool/bool1.expected @@ -0,0 +1,30 @@ + +unknown +( + + ; Functions + + ; Constants + + ; Arrays not yet supported + + +) + +unknown +( + + ; Functions + + ; Constants + +(define-fun p () Bool true) + +(define-fun q () Bool true) + +(define-fun nq () Bool true) + + ; Arrays not yet supported + + +) diff --git a/tests/models/bool/bool2.expected b/tests/models/bool/bool2.expected index e69de29bb..480cff179 100644 --- a/tests/models/bool/bool2.expected +++ b/tests/models/bool/bool2.expected @@ -0,0 +1,12 @@ + +unknown +( + + ; Functions + + ; Constants + + ; Arrays not yet supported + + +) diff --git a/tests/models/uf/uf1.expected b/tests/models/uf/uf1.expected index e69de29bb..ebcccf91c 100644 --- a/tests/models/uf/uf1.expected +++ b/tests/models/uf/uf1.expected @@ -0,0 +1,18 @@ + +unknown +( + + ; Functions + +(define-fun f ((arg_0 Int)) Int 0) + + ; Constants + +(define-fun a () Int 0) + +(define-fun b () Int 0) + + ; Arrays not yet supported + + +) diff --git a/tests/models/uf/uf2.expected b/tests/models/uf/uf2.expected index e69de29bb..ff0d5745c 100644 --- a/tests/models/uf/uf2.expected +++ b/tests/models/uf/uf2.expected @@ -0,0 +1,18 @@ + +unknown +( + + ; Functions + +(define-fun f ((arg_0 Int)) Int (ite (= arg_0 a) 2 0)) + + ; Constants + +(define-fun a () Int 0) + +(define-fun b () Int (- 2)) + + ; Arrays not yet supported + + +) diff --git a/tools/gentest.ml b/tools/gentest.ml index 7c182401d..332ea6a2b 100644 --- a/tools/gentest.ml +++ b/tools/gentest.ml @@ -315,7 +315,7 @@ let () = ; "--sat-solver=Tableaux" ; "--interpretation=last" ; timelimit ]) - ; ("runtest-quick", "models_ci", + ; ("runtest-ci", "models_ci", [ "--output=smtlib2" ; "--frontend=dolmen" ; "--sat-solver=Tableaux"