Skip to content

Commit 7dcc24f

Browse files
committed
Avoid storing a constant description in dry run solvert
We may as well just return a literal in the function implementation if the member variable will always be assigned the same literal value.
1 parent 7e76d47 commit 7dcc24f

File tree

3 files changed

+7
-10
lines changed

3 files changed

+7
-10
lines changed

src/solvers/smt2_incremental/smt_solver_process.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ smt_piped_solver_processt::smt_piped_solver_processt(
2020
{
2121
}
2222

23-
const std::string &smt_piped_solver_processt::description()
23+
std::string smt_piped_solver_processt::description()
2424
{
2525
return command_line_description;
2626
}
@@ -87,9 +87,9 @@ smt_incremental_dry_run_solvert::smt_incremental_dry_run_solvert(
8787
{
8888
}
8989

90-
const std::string &smt_incremental_dry_run_solvert::description()
90+
std::string smt_incremental_dry_run_solvert::description()
9191
{
92-
return desc;
92+
return "SMT2 incremental dry-run";
9393
}
9494

9595
void smt_incremental_dry_run_solvert::send(const smt_commandt &smt_command)

src/solvers/smt2_incremental/smt_solver_process.h

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ class smt_commandt;
1717
class smt_base_solver_processt
1818
{
1919
public:
20-
virtual const std::string &description() = 0;
20+
virtual std::string description() = 0;
2121

2222
/// \brief Converts given SMT2 command to SMT2 string and sends it to the
2323
/// solver process.
@@ -44,7 +44,7 @@ class smt_piped_solver_processt : public smt_base_solver_processt
4444
message_handlert &message_handler,
4545
std::unique_ptr<std::ostream> out_stream);
4646

47-
const std::string &description() override;
47+
std::string description() override;
4848

4949
void send(const smt_commandt &smt_command) override;
5050

@@ -81,7 +81,7 @@ class smt_incremental_dry_run_solvert : public smt_base_solver_processt
8181
std::ostream &out_stream,
8282
std::unique_ptr<std::ostream> file_stream);
8383

84-
const std::string &description() override;
84+
std::string description() override;
8585

8686
void send(const smt_commandt &smt_command) override;
8787

@@ -98,9 +98,6 @@ class smt_incremental_dry_run_solvert : public smt_base_solver_processt
9898
std::unique_ptr<std::ostream> file_stream;
9999
/// The output stream reference to print the SMT formula to.
100100
std::ostream &out_stream;
101-
102-
/// Description of the current solver
103-
const std::string desc = "SMT2 incremental dry-run";
104101
};
105102

106103
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ class smt_mock_solver_processt : public smt_base_solver_processt
7474
{
7575
}
7676

77-
const std::string &description() override
77+
std::string description() override
7878
{
7979
UNREACHABLE;
8080
}

0 commit comments

Comments
 (0)