From ca2497eecb837205861179599ebaa0bf3ba98cf4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 May 2022 11:59:37 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/ast.h | 5 ++--- src/smt/smt_context.cpp | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index 3cb90193f..79a3cebc7 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1914,9 +1914,8 @@ public: return mk_fresh_const(prefix.c_str(), s, skolem); } - app * mk_fresh_const(symbol const& prefix, sort * s, bool skolem = true) { - auto str = prefix.str(); - return mk_fresh_const(str.c_str(), s, skolem); + app * mk_fresh_const(symbol const& prefix, sort * s, bool skolem = true) { + return mk_const(mk_fresh_func_decl(prefix, symbol::null, 0, nullptr, s, skolem)); } symbol mk_fresh_var_name(char const * prefix = nullptr); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 3e444bec7..49c76ca53 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3168,7 +3168,7 @@ namespace smt { } else { expr_ref proxy(m), fml(m); - proxy = m.mk_fresh_const("proxy", m.mk_bool_sort()); + proxy = m.mk_fresh_const(symbol(), m.mk_bool_sort()); fml = m.mk_implies(proxy, e); m_asserted_formulas.assert_expr(fml); asm2proxy.push_back(std::make_pair(e, proxy));