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)
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);
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);