summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-04-27 17:04:49 -0500
committerGitHub <noreply@github.com>2020-04-27 15:04:49 -0700
commit30c0e8689a1e5f1ae160cde17d8124c86ead1568 (patch)
tree092585e7eaf2ac0e739d1731f73e58d98400551a
parentdc9b11c33d0f3283b82f2c87bfd7dd4c7126b0d0 (diff)
Fix sygus unit (#4371)
-rw-r--r--test/unit/api/solver_black.h2
1 files changed, 1 insertions, 1 deletions
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback