minor tweaks to last commit, testing infrastructure
authorMorgan Deters <mdeters@gmail.com>
Mon, 15 Nov 2010 20:24:35 +0000 (20:24 +0000)
committerMorgan Deters <mdeters@gmail.com>
Mon, 15 Nov 2010 20:24:35 +0000 (20:24 +0000)
src/Makefile.am
test/regress/regress0/push-pop/Makefile
test/regress/regress0/push-pop/test.00.cvc
test/regress/regress0/push-pop/test.01.cvc

index 069a446e688cc3b18afb7a5cceec4d0ae2f36cbe..8224deb8f864052421ff665453cdad44531b0de5 100644 (file)
@@ -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
index cd5bcd3e32518fa3300e18c9e69e0337aa9c045f..823a14011f4467d0b7666d35574beb41c35007e6 100644 (file)
@@ -1,4 +1,4 @@
-topdir = ../../../push-pop
+topdir = ../../../..
 srcdir = test/regress/regress0/push-pop
 
 include $(topdir)/Makefile.subdir
index 83634925101285a076654de7f166161e019b08b6..38d72022754f914c8bc45fc27f76a0f3bd88ffb9 100644 (file)
@@ -2,7 +2,10 @@ x: BOOLEAN;
 
 PUSH;
 ASSERT x;
+% EXPECT: sat
 CHECKSAT;
 POP;
 ASSERT (NOT x);
+% EXPECT: unsat
 CHECKSAT;
+% EXIT: 20
index 6110c6576f4b88e507cc42ca3c91a8e0fed79eff..90be7d7847904c012d30595edee5a9969470f129 100644 (file)
@@ -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