Actually add and run the tests

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'

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
+
+
+)

tests/models/bool/bool2.expected

@@ -0,0 +1,12 @@
+
+unknown
+(
+
+ ; Functions
+
+ ; Constants
+
+ ; Arrays not yet supported
+
+
+)

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
+
+
+)

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
+
+
+)

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"