@@ -203,8 +203,10 @@ compute_inverse_function(const exprt &qvar, const exprt &val, const exprt &f)
203
203
// / \param str: an array of characters
204
204
// / \param val: an index expression
205
205
// / \return instantiated formula
206
- exprt
207
- instantiate (const string_constraintt &axiom, const exprt &str, const exprt &val)
206
+ exprt instantiate (
207
+ const string_constraintt &axiom,
208
+ const exprt &str,
209
+ const exprt &val)
208
210
{
209
211
exprt::operandst conjuncts;
210
212
for (const auto &index : find_indexes (axiom.body , str, axiom.univ_var ))
@@ -213,9 +215,9 @@ instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val)
213
215
compute_inverse_function (axiom.univ_var , val, index);
214
216
implies_exprt instance (
215
217
and_exprt (
216
- binary_relation_exprt (axiom.univ_var , ID_ge, axiom.lower_bound ),
217
- binary_relation_exprt (axiom.univ_var , ID_lt, axiom.upper_bound )),
218
- axiom.body );
218
+ binary_relation_exprt (axiom.univ_var , ID_ge, axiom.lower_bound ),
219
+ binary_relation_exprt (axiom.univ_var , ID_lt, axiom.upper_bound )),
220
+ axiom.body );
219
221
replace_expr (axiom.univ_var , univ_var_value, instance);
220
222
conjuncts.push_back (instance);
221
223
}
0 commit comments