diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 19b488239..8f436bf8a 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -395,8 +395,7 @@ extern "C" { Z3_string s) { Z3_TRY; LOG_Z3_fixedpoint_from_string(c, d, s); - std::string str(s); - std::istringstream is(str); + std::istringstream is(s); RETURN_Z3(Z3_fixedpoint_from_stream(c, d, is)); Z3_CATCH_RETURN(nullptr); } diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index ebbe1a3db..5854bdaca 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -383,8 +383,7 @@ extern "C" { Z3_string s) { Z3_TRY; //LOG_Z3_optimize_from_string(c, d, s); - std::string str(s); - std::istringstream is(str); + std::istringstream is(s); Z3_optimize_from_stream(c, d, is, nullptr); Z3_CATCH; } diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp index 1454525d6..2d0770903 100644 --- a/src/api/api_params.cpp +++ b/src/api/api_params.cpp @@ -116,7 +116,7 @@ extern "C" { RESET_ERROR_CODE(); std::ostringstream buffer; to_params(p)->m_params.display(buffer); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } @@ -208,7 +208,7 @@ extern "C" { buffer << to_param_descrs_ptr(p)->get_param_name(i); } buffer << ")"; - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 00fe1cd8b..2510d5e17 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -157,8 +157,7 @@ extern "C" { Z3_ast_vector Z3_API Z3_parser_context_from_string(Z3_context c, Z3_parser_context pc, Z3_string str) { Z3_TRY; LOG_Z3_parser_context_from_string(c, pc, str); - std::string s(str); - std::istringstream is(s); + std::istringstream is(str); auto& ctx = to_parser_context(pc)->ctx; Z3_ast_vector r = Z3_parser_context_parse_stream(c, ctx, false, is); RETURN_Z3(r); @@ -202,8 +201,7 @@ extern "C" { Z3_func_decl const decls[]) { Z3_TRY; LOG_Z3_parse_smtlib2_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls); - std::string s(str); - std::istringstream is(s); + std::istringstream is(str); Z3_ast_vector r = parse_smtlib2_stream(false, c, is, num_sorts, sort_names, sorts, num_decls, decl_names, decls); RETURN_Z3(r); Z3_CATCH_RETURN(nullptr); @@ -243,8 +241,7 @@ extern "C" { ctx->set_solver_factory(mk_smt_strategic_solver_factory()); } scoped_ptr& ctx = mk_c(c)->cmd(); - std::string s(str); - std::istringstream is(s); + std::istringstream is(str); ctx->set_regular_stream(ous); ctx->set_diagnostic_stream(ous); cmd_context::scoped_redirect _redirect(*ctx); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 5edc42157..94d72462f 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -318,8 +318,7 @@ extern "C" { void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string c_str) { Z3_TRY; LOG_Z3_solver_from_string(c, s, c_str); - std::string str(c_str); - std::istringstream is(str); + std::istringstream is(c_str); if (is_dimacs_string(c_str)) { solver_from_dimacs_stream(c, s, is); }