c07192f844
- Add CVC4 support option and enabled by default - Unbreak on aarch64, sbrk is not used anymore - Remove build date to make the build reproducible - Pass maintainership to submitter - Pet `portlint -abct` PR: 231443 Submitted by: Greg V <greg@unrelenting.technology>
23 lines
945 B
C++
23 lines
945 B
C++
kind::IFF was removed in CVC4 1.6
|
|
--- src/Mixfix/variableGenerator.cc.orig 2018-09-17 10:44:35 UTC
|
|
+++ src/Mixfix/variableGenerator.cc
|
|
@@ -312,18 +312,7 @@ VariableGenerator::dagToCVC4(DagNode* dag)
|
|
//
|
|
case SMT_Symbol::EQUALS:
|
|
{
|
|
- //
|
|
- // Bizarrely CVC4 requires the IFF be used for Boolean equality so we need to
|
|
- // check the SMT type associated with our first argument sort to catch this case.
|
|
- //
|
|
- Sort* domainSort = s->getOpDeclarations()[0].getDomainAndRange()[0];
|
|
- SMT_Info::SMT_Type smtType = smtInfo.getType(domainSort);
|
|
- if (smtType == SMT_Info::NOT_SMT)
|
|
- {
|
|
- IssueWarning("term " << QUOTE(dag) << " does not belong to an SMT sort.");
|
|
- goto fail;
|
|
- }
|
|
- return exprManager->mkExpr(((smtType == SMT_Info::BOOLEAN) ? kind::IFF : kind::EQUAL), exprs[0], exprs[1]);
|
|
+ return exprManager->mkExpr(kind::EQUAL, exprs[0], exprs[1]);
|
|
}
|
|
case SMT_Symbol::NOT_EQUALS:
|
|
{
|