projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
80596bc
)
minor tweaks to last commit, testing infrastructure
author
Morgan Deters
<mdeters@gmail.com>
Mon, 15 Nov 2010 20:24:35 +0000
(20:24 +0000)
committer
Morgan Deters
<mdeters@gmail.com>
Mon, 15 Nov 2010 20:24:35 +0000
(20:24 +0000)
src/Makefile.am
patch
|
blob
|
history
test/regress/regress0/push-pop/Makefile
patch
|
blob
|
history
test/regress/regress0/push-pop/test.00.cvc
patch
|
blob
|
history
test/regress/regress0/push-pop/test.01.cvc
patch
|
blob
|
history
diff --git
a/src/Makefile.am
b/src/Makefile.am
index 069a446e688cc3b18afb7a5cceec4d0ae2f36cbe..8224deb8f864052421ff665453cdad44531b0de5 100644
(file)
--- 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 cd5bcd3e32518fa3300e18c9e69e0337aa9c045f..823a14011f4467d0b7666d35574beb41c35007e6 100644
(file)
--- 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 83634925101285a076654de7f166161e019b08b6..38d72022754f914c8bc45fc27f76a0f3bd88ffb9 100644
(file)
--- 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 6110c6576f4b88e507cc42ca3c91a8e0fed79eff..90be7d7847904c012d30595edee5a9969470f129 100644
(file)
--- 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