From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 18 Jun 2016 15:49:21 +0000 (-0500)
Subject: Fix unit test.
X-Git-Tag: cvc5-1.0.0~6049^2~6^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dc27675a9b9aa0346122390afdb28280f4495e9c;p=cvc5.git

Fix unit test.
---

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 89b0f054a..6ac1c5e32 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -442,6 +442,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
         enableTheory(THEORY_SETS);
         p += 2;
       }
+      if(!strncmp(p, "SEP", 3)) {
+        enableTheory(THEORY_SEP);
+        p += 3;
+      }
     }
   }
   if(*p != '\0') {
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 ) );