diff options
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 | ||||
| -rw-r--r-- | src/theory/logic_info.cpp | 2 | ||||
| -rw-r--r-- | test/unit/theory/logic_info_white.h | 14 |
3 files changed, 10 insertions, 10 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 761fe3b8c..e308db269 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -892,11 +892,11 @@ void SmtEngine::setLogicInternal() throw() { if (d_logic.isTheoryEnabled(theory::THEORY_ARITH) && !d_logic.isLinear()) { if (options::produceModels()) { - Notice() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << std::endl; + Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << std::endl; setOption("produce-models", SExpr("false")); } if (options::checkModels()) { - Notice() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << std::endl; + Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << std::endl; setOption("check-models", SExpr("false")); } } diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index d721d089e..d2cf57643 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -35,7 +35,7 @@ LogicInfo::LogicInfo() : d_sharingTheories(0), d_integers(true), d_reals(true), - d_linear(false), + d_linear(true),// for now, "everything enabled" doesn't include non-linear arith d_differenceLogic(false), d_locked(false) { 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() ); |