Skip to content

Commit 0983a0c

Browse files
author
Daniel Kroening
committed
make return type of get_quantifier_var_min obvious
This clarifies that the expression returned by get_quantifier_var_min is a constant -- request by @smowton.
1 parent c4f7a89 commit 0983a0c

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/solvers/flattening/boolbv_quantifier.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -140,8 +140,8 @@ instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
140140
return re;
141141
}
142142

143-
const auto min_i = get_quantifier_var_min(var_expr, re);
144-
const auto max_i = get_quantifier_var_max(var_expr, re);
143+
const optionalt<constant_exprt> min_i = get_quantifier_var_min(var_expr, re);
144+
const optionalt<constant_exprt> max_i = get_quantifier_var_max(var_expr, re);
145145

146146
if(!min_i.has_value() || !max_i.has_value())
147147
return nullopt;

0 commit comments

Comments
 (0)