summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-06-18 10:49:21 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-06-18 10:49:21 -0500
commitdc27675a9b9aa0346122390afdb28280f4495e9c (patch)
treeea6f33c6f0d9956dc5a5efa753d65469eac2802b /test
parentf5ed28fe24f6b887630a48dcf476c462c0c227a1 (diff)
Fix unit test.
Diffstat (limited to 'test')
-rw-r--r--test/unit/theory/logic_info_white.h7
1 files changed, 4 insertions, 3 deletions
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 6332563ed..3baa43dff 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -514,13 +514,13 @@ public:
info.arithOnlyLinear();
info.disableIntegers();
info.lock();
- TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVFPDTLRA" );
+ TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVFPDTLRASEP" );
info = info.getUnlockedCopy();
TS_ASSERT( !info.isLocked() );
info.disableQuantifiers();
info.lock();
- TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFBVFPDTLRA" );
+ TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFBVFPDTLRASEP" );
info = info.getUnlockedCopy();
TS_ASSERT( !info.isLocked() );
@@ -529,13 +529,14 @@ public:
info.enableIntegers();
info.disableReals();
info.lock();
- TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFFPLIA" );
+ TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFFPLIASEP" );
info = info.getUnlockedCopy();
TS_ASSERT( !info.isLocked() );
info.disableTheory(THEORY_ARITH);
info.disableTheory(THEORY_UF);
info.disableTheory(THEORY_FP);
+ info.disableTheory(THEORY_SEP);
info.lock();
TS_ASSERT_EQUALS( info.getLogicString(), "QF_AX" );
TS_ASSERT( info.isPure( THEORY_ARRAY ) );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback