Skip to content

Commit 405b639

Browse files
author
Thomas Kiley
committed
Fix supporting array_equal for non-matching types/sizes
Here the goal is to simplify the expression for __CPROVER_array_equal for things that are trivailly different, but we make it false = <complex expression>, which leads the result to simply be non-deterministic
1 parent 9fa5bf2 commit 405b639

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/goto-symex/symex_other.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -240,7 +240,7 @@ void goto_symext::symex_other(
240240

241241
// check for size (or type) mismatch
242242
if(array1.type() != array2.type())
243-
assignment.lhs() = false_exprt();
243+
assignment.rhs() = false_exprt();
244244

245245
symex_assign(state, assignment);
246246
}

0 commit comments

Comments
 (0)