mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 20:18:18 +00:00
remove output
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f6ab5a61ac
commit
046b80f6a4
|
@ -345,7 +345,6 @@ void proto_model::compress() {
|
||||||
void proto_model::complete_partial_func(func_decl * f, bool use_fresh) {
|
void proto_model::complete_partial_func(func_decl * f, bool use_fresh) {
|
||||||
func_interp * fi = get_func_interp(f);
|
func_interp * fi = get_func_interp(f);
|
||||||
if (fi && fi->is_partial()) {
|
if (fi && fi->is_partial()) {
|
||||||
verbose_stream() << "complete " << f->get_name() << " " << use_fresh << "\n";
|
|
||||||
expr * else_value;
|
expr * else_value;
|
||||||
if (use_fresh) {
|
if (use_fresh) {
|
||||||
else_value = get_fresh_value(f->get_range());
|
else_value = get_fresh_value(f->get_range());
|
||||||
|
|
Loading…
Reference in a new issue