summaryrefslogtreecommitdiff
path: root/src/smt/command.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r--src/smt/command.cpp22
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();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback