@@ -114,13 +114,15 @@ void goto_convertt::rewrite_boolean(exprt &expr)
114114 " ' must be Boolean, but got " ,
115115 irep_pretty_diagnosticst{expr});
116116
117+ const source_locationt source_location = expr.find_source_location ();
118+
117119 // re-write "a ==> b" into a?b:1
118120 if (auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
119121 {
120122 expr = if_exprt{
121123 std::move (implies->lhs ()),
122124 std::move (implies->rhs ()),
123- true_exprt{},
125+ true_exprt{}. with_source_location (source_location) ,
124126 bool_typet{}};
125127 return ;
126128 }
@@ -135,6 +137,8 @@ void goto_convertt::rewrite_boolean(exprt &expr)
135137 else // ID_or
136138 tmp = false_exprt ();
137139
140+ tmp.add_source_location () = source_location;
141+
138142 exprt::operandst &ops = expr.operands ();
139143
140144 // start with last one
@@ -146,17 +150,21 @@ void goto_convertt::rewrite_boolean(exprt &expr)
146150 DATA_INVARIANT_WITH_DIAGNOSTICS (
147151 op.is_boolean (),
148152 " boolean operators must have only boolean operands" ,
149- expr. find_source_location () );
153+ source_location );
150154
151155 if (expr.id () == ID_and)
152156 {
153- if_exprt if_e (op, tmp, false_exprt ());
157+ exprt if_e =
158+ if_exprt{op, tmp, false_exprt{}.with_source_location (source_location)}
159+ .with_source_location (source_location);
154160 tmp.swap (if_e);
155161 continue ;
156162 }
157163 if (expr.id () == ID_or)
158164 {
159- if_exprt if_e (op, true_exprt (), tmp);
165+ exprt if_e =
166+ if_exprt{op, true_exprt{}.with_source_location (source_location), tmp}
167+ .with_source_location (source_location);
160168 tmp.swap (if_e);
161169 continue ;
162170 }
0 commit comments