build: add tests that need smt

ehildenb · Sep 25, 2018 · 0f7c4e4 · 0f7c4e4
1 parent e7b44af
commit 0f7c4e4
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/build b/build
@@ -121,12 +121,21 @@ build_test_smt() {
     build_maude_cvc4
     build_tangle
     build_test tests/Misc/smtTest
+    build_test tests/tools/meta/nelson-oppen/hereditarily-finite-set
+    build_test tests/tools/meta/nelson-oppen/integer-list
+    build_test tests/tools/meta/nelson-oppen/lexical-trichotomy-law
+    ## CVC4 cannot handle the non-linear arithmetic
+	# build_test tests/tools/meta/nelson-oppen/matrix
 
     build_clean
     build_deps
     build_maude_yices2
     build_tangle
     build_test tests/Misc/smtTest
+    build_test tests/tools/meta/nelson-oppen/hereditarily-finite-set
+    build_test tests/tools/meta/nelson-oppen/integer-list
+    build_test tests/tools/meta/nelson-oppen/lexical-trichotomy-law
+    build_test tests/tools/meta/nelson-oppen/matrix
 
     git checkout -- src/Mixfix/tokenizer.cc
 }