From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 5 Jul 2017 21:07:04 +0000 (-0500)
Subject: Update unit test, news.
X-Git-Tag: cvc5-1.0.0~5747
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ad3d7ccf4be2d59b6f7b60b593dd2c30445828ec;p=cvc5.git

Update unit test, news.
---

diff --git a/NEWS b/NEWS
index 8c3bcc2aa..ff135d1ce 100644
--- a/NEWS
+++ b/NEWS
@@ -13,6 +13,7 @@ Changes since 1.4
 * A new theory of sets with cardinality and relations.
 * A new theory of strings.
 * Support for unsat cores.
+* Support for separation logic constraints.
 * Simplification mode "incremental" no longer supported.
 * Support for array constants in constraints.
 * Syntax for array models has changed in some language front-ends.
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index e8d297b59..a3e632be2 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -420,7 +420,7 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
-    TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED
+    TS_ASSERT( !info.isLinear() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
@@ -438,7 +438,7 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
-    TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED
+    TS_ASSERT( !info.isLinear() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
@@ -470,7 +470,7 @@ public:
     TS_ASSERT_THROWS( info.isQuantified(), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.isLinear(), CVC4::IllegalArgumentException );// for now, nonlinear not included in ALL_SUPPORTED
+    TS_ASSERT_THROWS( !info.isLinear(), CVC4::IllegalArgumentException );
 
     info.lock();
     TS_ASSERT( info.isLocked() );
@@ -495,7 +495,7 @@ public:
     TS_ASSERT( info.isQuantified() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
-    TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED
+    TS_ASSERT( !info.isLinear() );
 
     TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( info.disableIntegers(), CVC4::IllegalArgumentException );
@@ -596,7 +596,7 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
-    TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED
+    TS_ASSERT( !info.isLinear() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
@@ -615,7 +615,7 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
-    TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED
+    TS_ASSERT( !info.isLinear() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );