Skip to content

Commit c4ccf66

Browse files
committed
Fix "Include What You Use" complaint
1 parent 9fcc737 commit c4ccf66

File tree

3 files changed

+2
-3
lines changed

3 files changed

+2
-3
lines changed

regression/cbmc-incr-smt2/structs/large_array_of_struct_nondet_index.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ line 17 assertion struct_array\[x\]\.eggs \+ struct_array\[x\]\.ham != 11\: FAIL
99
\{\s*\.eggs=\d+,\s*\.ham=7\s*\}
1010
\{\s*\.eggs=\d+,\s*\.ham=8\s*\}
1111
x=\d{1,4}\s
12-
struct_array\[\(signed long int\)x\]\.eggs=3
12+
struct_array\[\(signed (long )+int\)x\]\.eggs=3
1313
--
1414
--
1515
This test covers support for examples with large arrays of structs using nondet

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@
44

55
#include <util/arith_tools.h>
66
#include <util/byte_operators.h>
7-
#include <util/expr.h>
87
#include <util/namespace.h>
98
#include <util/nodiscard.h>
109
#include <util/range.h>

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
77
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
88

9+
#include <util/expr.h> // Needed for `exprt` values. IWYU pragma: keep
910
#include <util/message.h>
10-
#include <util/std_expr.h>
1111

1212
#include <solvers/smt2_incremental/ast/smt_terms.h>
1313
#include <solvers/smt2_incremental/encoding/struct_encoding.h>

0 commit comments

Comments
 (0)