Fix ambiguous overload in unit test (#4582)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 8 Jun 2020 23:38:47 +0000 (16:38 -0700)
committerGitHub <noreply@github.com>
Mon, 8 Jun 2020 23:38:47 +0000 (18:38 -0500)
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

index 257c286694c94e3ffebb306996679a4080c11200..d53ef83030e627c78a17063b0dcc3938432b2c39 100644 (file)
@@ -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);