diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml index c60851c3471a5375bf6a5185021847bda3afb7dd..8c0b78e2e1d543de22177bbbb65cbac34307617c 100644 --- a/src/plugins/e-acsl/env.ml +++ b/src/plugins/e-acsl/env.ml @@ -157,7 +157,6 @@ let new_var ?(global=false) env t ty mk_stmts = match t with | None -> raise No_term | Some t -> - Options.feedback "memoized %a" Term.pretty t; Term.Map.find t local_env.mpz_tbl.new_exps, env with Not_found | No_term -> do_new_var ~global env t ty mk_stmts diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle index 6728e58d32b5bf86fae6f1426142f898328ac304..42f8891516ecf6aef1553d6d8ba96421deaddda5 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle @@ -1,9 +1,4 @@ -[e-acsl] memoized \old(x) -[e-acsl] memoized \old(x) -[e-acsl] memoized \old(x)-\old(x) tests/e-acsl-runtime/result.i:7:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable -[e-acsl] memoized \result -[e-acsl] memoized 0 [value] Analyzing a complete application starting at main [value] Computing initial state [value] Initial state computed