diff --git a/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc b/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc index 7149815c6d9..4fe2cf25dde 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 dfcc-only 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 6f9b34dd89c..6306416f3bf 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 dfcc-only 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 803cf47eb6a..6dd6cf7e681 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); } }