From 0f7c4e4acf2f8ca5d4ca5b6d2566eb478cc4d707 Mon Sep 17 00:00:00 2001
From: Nishant Rodrigues <nishantjr@gmail.com>
Date: Tue, 25 Sep 2018 18:08:47 -0500
Subject: [PATCH] build: add tests that need smt

---
 build | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/build b/build
index af1ba440..2957f65f 100755
--- 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
 }