File tree Expand file tree Collapse file tree 3 files changed +9
-3
lines changed
smt2_incremental/encoding Expand file tree Collapse file tree 3 files changed +9
-3
lines changed Original file line number Diff line number Diff line change @@ -211,6 +211,7 @@ SRC = $(BOOLEFORCE_SRC) \
211
211
smt2_incremental/smt2_incremental_decision_procedure.cpp \
212
212
smt2_incremental/encoding/struct_encoding.cpp \
213
213
smt2_incremental/encoding/enum_encoding.cpp \
214
+ smt2_incremental/encoding/nondet_padding.cpp \
214
215
smt2_incremental/theories/smt_array_theory.cpp \
215
216
smt2_incremental/theories/smt_bit_vector_theory.cpp \
216
217
smt2_incremental/theories/smt_core_theory.cpp \
Original file line number Diff line number Diff line change
1
+ // Author: Diffblue Ltd.
2
+
3
+ #include " nondet_padding.h"
4
+
5
+ const irep_idt nondet_padding_exprt::ID_nondet_padding = " nondet_padding" ;
Original file line number Diff line number Diff line change 13
13
class nondet_padding_exprt ;
14
14
void validate_expr (const nondet_padding_exprt &padding);
15
15
16
- const irep_idt ID_nondet_padding = " nondet_padding" ;
17
-
18
16
class nondet_padding_exprt : public expr_protectedt
19
17
{
20
18
public:
19
+ static const irep_idt ID_nondet_padding;
20
+
21
21
explicit nondet_padding_exprt (typet type)
22
22
: expr_protectedt{ID_nondet_padding, std::move (type)}
23
23
{
@@ -28,7 +28,7 @@ class nondet_padding_exprt : public expr_protectedt
28
28
template <>
29
29
inline bool can_cast_expr<nondet_padding_exprt>(const exprt &base)
30
30
{
31
- return base.id () == ID_nondet_padding;
31
+ return base.id () == nondet_padding_exprt:: ID_nondet_padding;
32
32
}
33
33
34
34
inline void validate_expr (const nondet_padding_exprt &padding)
You can’t perform that action at this time.
0 commit comments