diff --git a/src/goto-symex/memory_model_pso.cpp b/src/goto-symex/memory_model_pso.cpp index 2ef634e208c..d8487e629fd 100644 --- a/src/goto-symex/memory_model_pso.cpp +++ b/src/goto-symex/memory_model_pso.cpp @@ -16,7 +16,7 @@ void memory_model_psot::operator()(symex_target_equationt &equation) statistics() << "Adding PSO constraints" << eom; build_event_lists(equation); - build_clock_type(equation); + build_clock_type(); read_from(equation); write_serialization_external(equation); diff --git a/src/goto-symex/memory_model_sc.cpp b/src/goto-symex/memory_model_sc.cpp index cfe30c80766..a09f9652f30 100644 --- a/src/goto-symex/memory_model_sc.cpp +++ b/src/goto-symex/memory_model_sc.cpp @@ -18,7 +18,7 @@ void memory_model_sct::operator()(symex_target_equationt &equation) statistics() << "Adding SC constraints" << eom; build_event_lists(equation); - build_clock_type(equation); + build_clock_type(); read_from(equation); write_serialization_external(equation); diff --git a/src/goto-symex/memory_model_tso.cpp b/src/goto-symex/memory_model_tso.cpp index 5b390267086..8bf28a28813 100644 --- a/src/goto-symex/memory_model_tso.cpp +++ b/src/goto-symex/memory_model_tso.cpp @@ -19,7 +19,7 @@ void memory_model_tsot::operator()(symex_target_equationt &equation) statistics() << "Adding TSO constraints" << eom; build_event_lists(equation); - build_clock_type(equation); + build_clock_type(); read_from(equation); write_serialization_external(equation); diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp index bd05a170109..fb9529a83fb 100644 --- a/src/goto-symex/partial_order_concurrency.cpp +++ b/src/goto-symex/partial_order_concurrency.cpp @@ -161,8 +161,7 @@ symbol_exprt partial_order_concurrencyt::clock( return symbol_exprt(identifier, clock_type); } -void partial_order_concurrencyt::build_clock_type( - const symex_target_equationt &equation) +void partial_order_concurrencyt::build_clock_type() { assert(!numbering.empty()); diff --git a/src/goto-symex/partial_order_concurrency.h b/src/goto-symex/partial_order_concurrency.h index adb82366cbd..759e240b98b 100644 --- a/src/goto-symex/partial_order_concurrency.h +++ b/src/goto-symex/partial_order_concurrency.h @@ -77,7 +77,7 @@ class partial_order_concurrencyt:public messaget // produce a clock symbol for some event typet clock_type; symbol_exprt clock(event_it e, axiomt axiom); - void build_clock_type(const symex_target_equationt &); + void build_clock_type(); // preprocess and add a constraint to equation void add_constraint(