Skip to content

Commit

Permalink
Ugly commit.
Browse files Browse the repository at this point in the history
  • Loading branch information
vakaras committed Jan 27, 2023
1 parent d0b444f commit b5f391a
Showing 1 changed file with 1 addition and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -126,14 +126,13 @@ impl<'a> ProcedureExecutor<'a> {
procedure: vir_low::ProcedureDecl,
new_procedures: &mut Vec<vir_low::ProcedureDecl>,
) -> SpannedEncodingResult<()> {
eprintln!("Executing procedure {}", procedure.name);
debug!("Executing procedure {}", procedure.name);
// Intern all non-aliased predicates.
for address in self
.program_context
.get_non_aliased_memory_block_addresses()
{
assert!(address.is_heap_independent());
eprintln!("non-aliased address: {}", address);
use vir_low::macros::*;
let address_is_non_aliased = ty!(Bool);
let address_non_aliased_call = expr! {
Expand Down

0 comments on commit b5f391a

Please sign in to comment.