From cf6bc6c57dd579b8f75b7d20922eda0eaa92b2f7 Mon Sep 17 00:00:00 2001
From: Martin Brain <martin.brain@cs.ox.ac.uk>
Date: Wed, 3 Dec 2014 21:29:43 -0500
Subject: Floating point infrastructure.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
---
 test/unit/theory/logic_info_white.h | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'test/unit/theory')

diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 007378528..efc7c5582 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -512,13 +512,13 @@ public:
     info.arithOnlyLinear();
     info.disableIntegers();
     info.lock();
-    TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTLRA" );
+    TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVFPDTLRA" );
 
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
     info.disableQuantifiers();
     info.lock();
-    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFBVDTLRA" );
+    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFBVFPDTLRA" );
 
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
@@ -527,12 +527,13 @@ public:
     info.enableIntegers();
     info.disableReals();
     info.lock();
-    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFLIA" );
+    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFFPLIA" );
 
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
     info.disableTheory(THEORY_ARITH);
     info.disableTheory(THEORY_UF);
+    info.disableTheory(THEORY_FP);
     info.lock();
     TS_ASSERT_EQUALS( info.getLogicString(), "QF_AX" );
     TS_ASSERT( info.isPure( THEORY_ARRAY ) );
-- 
cgit v1.2.3