diff --git a/regression/contracts/assigns_replace_03/test.desc b/regression/contracts/assigns_replace_03/test.desc index 9cf224b7c34..93cd2e13787 100644 --- a/regression/contracts/assigns_replace_03/test.desc +++ b/regression/contracts/assigns_replace_03/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --replace-all-calls-with-contracts ^EXIT=0$ @@ -7,7 +7,3 @@ main.c -- -- This test checks that a havocked variable can be constrained by a function post-condition. - -Known Bug: -Currently, there is a bug when char variables are being passed to -__CPROVER_w_ok(). See GitHub issue #6106 for further details. diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 831ab0b0953..b7ef438ff25 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -1698,7 +1698,7 @@ goto_programt assigns_clauset::havoc_code( { // create the condition exprt condition = - not_exprt(w_ok_exprt(target_ptr, from_integer(0, integer_typet()))); + not_exprt(w_ok_exprt(target_ptr, from_integer(0, unsigned_int_type()))); havoc_statements.add(goto_programt::make_goto(z, condition, location)); } @@ -1775,8 +1775,8 @@ exprt assigns_clauset::compatible_expression( // target->compatible_expression(*called_target) would not be // checked on invalid called_targets. current_target_compatible = or_exprt( - not_exprt( - w_ok_exprt(called_target_ptr, from_integer(0, integer_typet()))), + not_exprt(w_ok_exprt( + called_target_ptr, from_integer(0, unsigned_int_type()))), target->compatible_expression(*called_target)); } else