summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorLiana Hadarean <lianahady@gmail.com>2013-03-19 22:09:55 -0400
committerLiana Hadarean <lianahady@gmail.com>2013-03-19 22:09:55 -0400
commitc30b3e2c03f9c3df51eb8d2e7cb6c72907cb77c0 (patch)
tree35ffaacc7ba2b0d2d7b6b4e47112fcd41f560b2d /test
parent4cd63abf2ab901ad8d1b1c2cc2e84707736b5659 (diff)
parent66175a0f0e8d9cf3bc89c3d422ef5b18b217a7da (diff)
merged master with dejan's constant evaluating equality engine
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/arith/miplib4.cvc3
-rw-r--r--test/system/Makefile.am2
-rw-r--r--test/unit/Makefile.am2
3 files changed, 5 insertions, 2 deletions
diff --git a/test/regress/regress0/arith/miplib4.cvc b/test/regress/regress0/arith/miplib4.cvc
index d56015222..2f7db1f54 100644
--- a/test/regress/regress0/arith/miplib4.cvc
+++ b/test/regress/regress0/arith/miplib4.cvc
@@ -5,9 +5,12 @@
tmp1 : INT;
x, y : BOOLEAN;
+% nonlinear combination, not eligible for miplib trick replacement
ASSERT NOT x AND (NOT y AND TRUE) => tmp1 = 0;
ASSERT x AND (NOT y AND TRUE) => tmp1 = 4;
ASSERT NOT x AND ( y AND TRUE) => tmp1 = 6;
ASSERT x AND ( y AND TRUE) => tmp1 = 12;
+ASSERT tmp1 > 10;
+
CHECKSAT;
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 0cd633dc6..e8e3f8c87 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -63,10 +63,10 @@ endif
AM_CPPFLAGS = \
-I. \
+ "-I@top_builddir@/src" \
"-I@top_srcdir@/src/include" \
"-I@top_srcdir@/lib" \
"-I@top_srcdir@/src" \
- "-I@top_builddir@/src" \
"-I@top_srcdir@/src/prop/minisat" \
-D __STDC_LIMIT_MACROS \
-D __STDC_FORMAT_MACROS \
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index a287b7520..a5530ab6d 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -68,10 +68,10 @@ if HAVE_CXXTESTGEN
AM_CPPFLAGS = \
-I. \
"-I@CXXTEST@" \
+ "-I@top_builddir@/src" \
"-I@top_srcdir@/src/include" \
"-I@top_srcdir@/lib" \
"-I@top_srcdir@/src" \
- "-I@top_builddir@/src" \
"-I@top_srcdir@/src/prop/minisat" \
-D __STDC_LIMIT_MACROS \
-D __STDC_FORMAT_MACROS \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback