minor tweaks to last commit, testing infrastructure

4 files changed, 11 insertions, 3 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 069a446e6..8224deb8f 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -17,7 +17,7 @@ AM_CPPFLAGS = \
 	-I@srcdir@/include -I@srcdir@ -I@builddir@
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
-SUBDIRS = lib expr util context theory prop smt printer . parser main
+SUBDIRS = lib expr util context theory prop smt . parser main
 
 lib_LTLIBRARIES = libcvc4.la
 noinst_LTLIBRARIES = libcvc4_noinst.la
diff --git a/test/regress/regress0/push-pop/Makefile b/test/regress/regress0/push-pop/Makefile
index cd5bcd3e3..823a14011 100644
--- a/test/regress/regress0/push-pop/Makefile
+++ b/test/regress/regress0/push-pop/Makefile
@@ -1,4 +1,4 @@
-topdir = ../../../push-pop
+topdir = ../../../..
 srcdir = test/regress/regress0/push-pop
 
 include $(topdir)/Makefile.subdir
diff --git a/test/regress/regress0/push-pop/test.00.cvc b/test/regress/regress0/push-pop/test.00.cvc
index 836349251..38d720227 100644
--- a/test/regress/regress0/push-pop/test.00.cvc
+++ b/test/regress/regress0/push-pop/test.00.cvc
@@ -2,7 +2,10 @@ x: BOOLEAN;
 
 PUSH;
 ASSERT x;
+% EXPECT: sat
 CHECKSAT;
 POP;
 ASSERT (NOT x);
+% EXPECT: unsat
 CHECKSAT;
+% EXIT: 20
diff --git a/test/regress/regress0/push-pop/test.01.cvc b/test/regress/regress0/push-pop/test.01.cvc
index 6110c6576..90be7d784 100644
--- a/test/regress/regress0/push-pop/test.01.cvc
+++ b/test/regress/regress0/push-pop/test.01.cvc
@@ -1,13 +1,18 @@
 x, y: BOOLEAN;
 
 ASSERT (x OR y);
+% EXPECT: sat
 CHECKSAT;
 PUSH;
 ASSERT (NOT x);
+% EXPECT: sat
 CHECKSAT;
 POP;
 PUSH;
 ASSERT (NOT y);
+% EXPECT: sat
 CHECKSAT;
 POP;
-CHECKSAT;
\ No newline at end of file
+% EXPECT: sat
+CHECKSAT;
+% EXIT: 10