mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
remove output
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
2dbf9bcab2
commit
63ea8efcfb
|
@ -538,7 +538,6 @@ namespace seq {
|
|||
expr_ref t_eq_empty = mk_eq_empty(t);
|
||||
expr_ref xsy = mk_concat(x, s, y);
|
||||
|
||||
verbose_stream() << s << " " << t << "\n";
|
||||
// add_clause(~mk_eq(t, s), i_eq_0);
|
||||
add_clause(cnt, i_eq_m1);
|
||||
add_clause(~t_eq_empty, s_eq_empty, i_eq_m1);
|
||||
|
|
Loading…
Reference in a new issue