Skip to content

Commit

Permalink
fix encoding of heap_load
Browse files Browse the repository at this point in the history
  • Loading branch information
zhuyutian57 committed Aug 20, 2024
1 parent fbd6603 commit 1a199d2
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion benchmark/case_0.c
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
int main(){
int * data = malloc(sizeof(int));
int * data2 = malloc(2*sizeof(int));
free(data2);
free(data);
int i = *(data + 1);
// int* j = NULL;
// int* i = j;
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/z3-slhv/z3_slhv_conv.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -279,7 +279,7 @@ z3_slhv_convt::convert_slhv_opts(
v1 = mk_fresh(mk_int_sort(), mk_fresh_name("tmp_val::"));

assert_ast(mk_subh(mk_pt(args[1], v1), args[0]));
return args[0];
return v1;
}
case expr2t::heap_contains_id:
{
Expand Down

1 comment on commit 1a199d2

@zhuyutian57
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

fix #1 and #3

Please sign in to comment.