diff options
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 5585ab48f..f27ed6e1f 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1602,7 +1602,7 @@ void GetValueCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->mkTerm(api::SEXPR, result); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -1680,7 +1680,7 @@ void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->mkTerm(api::SEXPR, sexprs); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -1813,7 +1813,7 @@ void BlockModelCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->blockModel(); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -1867,7 +1867,7 @@ void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->blockModelValues(d_terms); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -1913,7 +1913,7 @@ void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->getSmtEngine()->getProof(); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2318,7 +2318,7 @@ void GetUnsatAssumptionsCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->getUnsatAssumptions(); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2380,7 +2380,7 @@ void GetUnsatCoreCommand::invoke(api::Solver* solver, SymbolManager* sm) d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2615,7 +2615,7 @@ void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->setInfo(d_flag, d_value); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException&) + catch (api::CVC5ApiRecoverableException&) { // As per SMT-LIB spec, silently accept unknown set-info keys d_commandStatus = CommandSuccess::instance(); @@ -2657,7 +2657,7 @@ void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = sexprToString(solver->mkTerm(api::SEXPR, v)); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2716,7 +2716,7 @@ void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->setOption(d_flag, d_value); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException&) + catch (api::CVC5ApiRecoverableException&) { d_commandStatus = new CommandUnsupported(); } @@ -2754,7 +2754,7 @@ void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->getOption(d_flag); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException&) + catch (api::CVC5ApiRecoverableException&) { d_commandStatus = new CommandUnsupported(); } |