diff --git a/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc b/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc index 7149815c6d9c..aa9c9db10340 100644 --- a/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc +++ b/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE assigns.c --dfcc main --apply-loop-contracts ^EXIT=0$ diff --git a/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc index 6f9b34dd89c1..bd0eef260ac8 100644 --- a/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc +++ b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE side_effect.c --dfcc main --apply-loop-contracts ^EXIT=0$ diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 803cf47eb6ae..6dd6cf7e6817 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -250,7 +250,7 @@ void insert_before_and_update_jumps( const auto new_target = destination.insert_before(target, i); for(auto it : target->incoming_edges) { - if(it->is_goto()) + if(it->is_goto() && it->get_target() == target) it->set_target(new_target); } }