diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-11-10 16:41:01 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-11-10 16:41:01 +0000 |
| commit | 3169a068f1a0a6b1f8cc902847d106664d6c0bd9 (patch) | |
| tree | 3d0ffedb4dff63cab04e5b3c867eaa4b9aec5dc7 /test/unit | |
| parent | e1068a39e661d89d20b47e15fa7d142a28733196 (diff) | |
Updates to Clark's commit r4540:
* ALL_SUPPORTED/QF_ALL_SUPPORTED don't include nonlinear
* Change "Notice" to "Warning" when produce-models turned off due to non-linear
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/theory/logic_info_white.h | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index ba498c032..430a2a164 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -418,7 +418,7 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); + TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( info.areRealsUsed() ); @@ -436,7 +436,7 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); + TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( info.areRealsUsed() ); @@ -470,11 +470,11 @@ 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 ); + TS_ASSERT_THROWS( info.isLinear(), CVC4::IllegalArgumentException );// for now, nonlinear not included in ALL_SUPPORTED info.lock(); TS_ASSERT( info.isLocked() ); - TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTNIRA" ); + TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTLIRA" );// for now, nonlinear not included in ALL_SUPPORTED TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isTheoryEnabled( THEORY_BUILTIN ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); @@ -497,7 +497,7 @@ public: TS_ASSERT( info.isQuantified() ); TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT( ! info.isLinear() ); + TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( info.disableIntegers(), CVC4::IllegalArgumentException ); @@ -594,7 +594,7 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); + TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( info.areRealsUsed() ); @@ -613,7 +613,7 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); + TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( info.areRealsUsed() ); |