diff --git a/src/solvers/smt2_incremental/ast/smt_terms.h b/src/solvers/smt2_incremental/ast/smt_terms.h index c8b2d375a37..eef3b3dbb0f 100644 --- a/src/solvers/smt2_incremental/ast/smt_terms.h +++ b/src/solvers/smt2_incremental/ast/smt_terms.h @@ -153,28 +153,15 @@ class smt_function_application_termt : public smt_termt { }; - /// Overload for when \p functiont does not have indices. - template - static std::vector - indices(const functiont &function, const std::false_type &has_indices) - { - return {}; - } - - /// Overload for when \p functiont has indices member function. - template - static std::vector - indices(const functiont &function, const std::true_type &has_indices) - { - return function.indices(); - } - - /// Returns `function.indices` if `functiont` has an `indices` member function - /// or returns an empty collection otherwise. + /// Returns `function.indices()` if `functiont` has an `indices` member + /// function or returns an empty collection otherwise. template static std::vector indices(const functiont &function) { - return indices(function, has_indicest{}); + if constexpr(has_indicest::value) + return function.indices(); + else + return {}; } public: