diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/arith/integers/Makefile.am | 2 | ||||
-rw-r--r-- | test/unit/theory/theory_arith_white.h | 2 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 31 |
3 files changed, 6 insertions, 29 deletions
diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am index ccfeb51f1..d55e12fbc 100644 --- a/test/regress/regress0/arith/integers/Makefile.am +++ b/test/regress/regress0/arith/integers/Makefile.am @@ -18,7 +18,6 @@ TESTS = \ arith-int-013.cvc \ arith-int-022.cvc \ arith-int-024.cvc \ - arith-int-041.cvc \ arith-int-042.cvc \ arith-int-042.min.cvc \ arith-int-047.cvc \ @@ -66,6 +65,7 @@ EXTRA_DIST = $(TESTS) \ arith-int-038.cvc \ arith-int-039.cvc \ arith-int-040.cvc \ + arith-int-041.cvc \ arith-int-043.cvc \ arith-int-044.cvc \ arith-int-045.cvc \ diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 4787dfd21..41d370aac 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -64,7 +64,7 @@ class TheoryArithWhite : public CxxTest::TestSuite { public: - TheoryArithWhite() : d_level(Theory::FULL_EFFORT), d_zero(0), d_one(1), debug(false) {} + TheoryArithWhite() : d_level(Theory::EFFORT_FULL), d_zero(0), d_one(1), debug(false) {} void fakeTheoryEnginePreprocess(TNode inp){ Node rewrite = inp; //FIXME this needs to enforce that inp is fully rewritten already! diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 76385219d..a737772ed 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -181,38 +181,15 @@ public: } void testEffort(){ - Theory::Effort m = Theory::MIN_EFFORT; - Theory::Effort q = Theory::QUICK_CHECK; - Theory::Effort s = Theory::STANDARD; - Theory::Effort f = Theory::FULL_EFFORT; - - TS_ASSERT( Theory::minEffortOnly(m)); - TS_ASSERT(!Theory::minEffortOnly(q)); - TS_ASSERT(!Theory::minEffortOnly(s)); - TS_ASSERT(!Theory::minEffortOnly(f)); - - TS_ASSERT(!Theory::quickCheckOnly(m)); - TS_ASSERT( Theory::quickCheckOnly(q)); - TS_ASSERT(!Theory::quickCheckOnly(s)); - TS_ASSERT(!Theory::quickCheckOnly(f)); - - TS_ASSERT(!Theory::standardEffortOnly(m)); - TS_ASSERT(!Theory::standardEffortOnly(q)); + Theory::Effort s = Theory::EFFORT_STANDARD; + Theory::Effort f = Theory::EFFORT_FULL; + TS_ASSERT( Theory::standardEffortOnly(s)); TS_ASSERT(!Theory::standardEffortOnly(f)); - TS_ASSERT(!Theory::fullEffort(m)); - TS_ASSERT(!Theory::fullEffort(q)); TS_ASSERT(!Theory::fullEffort(s)); TS_ASSERT( Theory::fullEffort(f)); - TS_ASSERT(!Theory::quickCheckOrMore(m)); - TS_ASSERT( Theory::quickCheckOrMore(q)); - TS_ASSERT( Theory::quickCheckOrMore(s)); - TS_ASSERT( Theory::quickCheckOrMore(f)); - - TS_ASSERT(!Theory::standardEffortOrMore(m)); - TS_ASSERT(!Theory::standardEffortOrMore(q)); TS_ASSERT( Theory::standardEffortOrMore(s)); TS_ASSERT( Theory::standardEffortOrMore(f)); } @@ -225,7 +202,7 @@ public: TS_ASSERT(!d_dummy->doneWrapper()); - d_dummy->check(Theory::FULL_EFFORT); + d_dummy->check(Theory::EFFORT_FULL); TS_ASSERT(d_dummy->doneWrapper()); } |