Skip to content

Commit 44a840b

Browse files
committed
SMT2 incremental back-end: don't use irep_full_hash
`irep_full_hash` would require also using `irep_full_eq`, but there is no need to consider comments in this context. This fixes the unexpected failures seen in runs like https://github.com/diffblue/cbmc/actions/runs/5069698268/jobs/9103685508.
1 parent d5e13f1 commit 44a840b

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@
3535
/// * supporting wider scope for the conversion of specific types of `exprt`,
3636
/// without inflating the parameter list / scope for all conversions.
3737
using sub_expression_mapt =
38-
std::unordered_map<exprt, smt_termt, irep_full_hash>;
38+
std::unordered_map<exprt, smt_termt, irep_hash>;
3939

4040
/// \brief Converts operator expressions with 2 or more operands to terms
4141
/// expressed as binary operator application.

src/solvers/smt2_incremental/type_size_mapping.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@
1515

1616
#include <unordered_map> // IWYU pragma: keep
1717

18-
using type_size_mapt = std::unordered_map<typet, smt_termt, irep_full_hash>;
18+
using type_size_mapt = std::unordered_map<typet, smt_termt, irep_hash>;
1919

2020
/// This function populates the (pointer) type -> size map.
2121
/// \param expression: the expression we're building the map for.

0 commit comments

Comments
 (0)