From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 27 Apr 2020 22:04:49 +0000 (-0500)
Subject: Fix sygus unit (#4371)
X-Git-Tag: cvc5-1.0.0~3338
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=30c0e8689a1e5f1ae160cde17d8124c86ead1568;p=cvc5.git

Fix sygus unit (#4371)
---

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 4b5480dba..bfbe201d2 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -1261,7 +1261,7 @@ void SolverBlack::testSynthFun()
   Sort null = d_solver->getNullSort();
   Sort boolean = d_solver->getBooleanSort();
   Sort integer = d_solver->getIntegerSort();
-  Sort boolToBool = d_solver->mkFunctionSort({boolean}, boolean);
+  Sort boolToBool = d_solver->mkFunctionSort(boolean, boolean);
 
   Term nullTerm;
   Term x = d_solver->mkVar(boolean);