From f515641c3b078185743aed831e2fe6c2759341fb Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 8 Jun 2020 16:38:47 -0700 Subject: Fix ambiguous overload in unit test (#4582) Fixes nightlies. The compiler version used for our nightlies (GCC 5.4.0) complains about mkFunctionSort({bSort}, bSort) being ambiguous because we have two variants of mkFunctionSort(): one that takes a single Sort and one that takes a vector of Sorts. This commit makes the function call unambiguous by removing the use of list initializations. --- test/unit/api/solver_black.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'test/unit') diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 257c28669..d53ef8303 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -1042,7 +1042,7 @@ void SolverBlack::testDefineFun() void SolverBlack::testDefineFunGlobal() { Sort bSort = d_solver->getBooleanSort(); - Sort fSort = d_solver->mkFunctionSort({bSort}, bSort); + Sort fSort = d_solver->mkFunctionSort(bSort, bSort); Term bTrue = d_solver->mkBoolean(true); // (define-fun f () Bool true) @@ -1120,7 +1120,7 @@ void SolverBlack::testDefineFunRec() void SolverBlack::testDefineFunRecGlobal() { Sort bSort = d_solver->getBooleanSort(); - Sort fSort = d_solver->mkFunctionSort({bSort}, bSort); + Sort fSort = d_solver->mkFunctionSort(bSort, bSort); d_solver->push(); Term bTrue = d_solver->mkBoolean(true); @@ -1217,7 +1217,7 @@ void SolverBlack::testDefineFunsRec() void SolverBlack::testDefineFunsRecGlobal() { Sort bSort = d_solver->getBooleanSort(); - Sort fSort = d_solver->mkFunctionSort({bSort}, bSort); + Sort fSort = d_solver->mkFunctionSort(bSort, bSort); d_solver->push(); Term bTrue = d_solver->mkBoolean(true); -- cgit v1.2.3