From eb5b1c4ba7f64f07a04b25382332096a80cee8db Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Mon, 11 Feb 2019 10:42:53 +0000 Subject: [PATCH] Remove invariant on `full_lhs_value` in printing `goto_tracet` This invariant in the printing is preventing other, otherwise usefull output from being printed, in the case where a goto trace has been produced which contains a `full_lhs_value` set to `nil` in an assignment step. --- src/goto-programs/json_goto_trace.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 46b761530c1..459adacfb67 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -132,9 +132,6 @@ void convert_decl( } else { - DATA_INVARIANT( - step.full_lhs_value.is_not_nil(), - "full_lhs_value in assignment must not be nil"); full_lhs_value = json(step.full_lhs_value, ns, ID_unknown); }