diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-25 11:47:38 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-03-25 09:47:38 -0700 |
| commit | c03e15c1b4ef6ec62209f2a4906cce5843e80c46 (patch) | |
| tree | 3446029246936a23004e734e5e2590bde37b87c6 /src/theory/uf | |
| parent | 9e9e6b8777047160ef7a1f2708a295aa503eb856 (diff) | |
Cleanup various exit calls (#1692)
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index b32a50eb4..76cb95867 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1147,9 +1147,10 @@ void SortModel::allocateCardinality( OutputChannel* out ){ //check for abort case if (options::ufssAbortCardinality() != -1 && d_aloc_cardinality >= options::ufssAbortCardinality()) { - Message() << "Maximum cardinality (" << options::ufssAbortCardinality() - << ") for finite model finding exceeded." << std::endl; - exit( 1 ); + std::stringstream ss; + ss << "Maximum cardinality (" << options::ufssAbortCardinality() + << ") for finite model finding exceeded." << std::endl; + throw LogicException(ss.str()); }else{ if( applyTotality( d_aloc_cardinality ) ){ //must generate new cardinality lemma term @@ -1231,7 +1232,7 @@ int SortModel::addSplit( Region* r, OutputChannel* out ){ } if( ss==b_t ){ Message() << "Bad split " << s << std::endl; - exit( 16 ); + AlwaysAssert(false); } } if( options::sortInference()) { |