diff options
author | Liana Hadarean <lianahady@gmail.com> | 2013-03-19 22:09:55 -0400 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2013-03-19 22:09:55 -0400 |
commit | c30b3e2c03f9c3df51eb8d2e7cb6c72907cb77c0 (patch) | |
tree | 35ffaacc7ba2b0d2d7b6b4e47112fcd41f560b2d /test | |
parent | 4cd63abf2ab901ad8d1b1c2cc2e84707736b5659 (diff) | |
parent | 66175a0f0e8d9cf3bc89c3d422ef5b18b217a7da (diff) |
merged master with dejan's constant evaluating equality engine
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/arith/miplib4.cvc | 3 | ||||
-rw-r--r-- | test/system/Makefile.am | 2 | ||||
-rw-r--r-- | test/unit/Makefile.am | 2 |
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 \ |