Index
| .<. | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| .>. | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| =/= | |
| 1 (Function) | SMTLib2.Core |
| 2 (Function) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| === | |
| 1 (Function) | SMTLib2.Core |
| 2 (Function) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| ==> | SMTLib2.Core |
| And | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| and | SMTLib2.Core |
| Annot | |
| 1 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 2 (Type/Class) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| annot | SMTLib2.Compat1 |
| App | |
| 1 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| app | SMTLib2.AST, SMTLib2 |
| assume | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Attr | |
| 1 (Type/Class) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 3 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| attrName | |
| 1 (Function) | SMTLib2.AST, SMTLib2 |
| 2 (Function) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| AttrVal | SMTLib2.AST, SMTLib2 |
| attrVal | |
| 1 (Function) | SMTLib2.AST, SMTLib2 |
| 2 (Function) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Bind | |
| 1 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Binder | |
| 1 (Type/Class) | SMTLib2.AST, SMTLib2 |
| 2 (Type/Class) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| binder | SMTLib2.Compat1 |
| bindSort | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bindType | SMTLib2.AST, SMTLib2 |
| bindVar | |
| 1 (Function) | SMTLib2.AST, SMTLib2 |
| 2 (Function) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bit0 | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bit1 | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bv | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvadd | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvand | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvashr | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvcomp | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvlshr | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvmul | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvnand | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvneg | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvnor | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvnot | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvor | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvsdiv | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvsge | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvsgt | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvshl | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvsle | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvslt | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvsmod | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvsrem | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvsub | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvudiv | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvuge | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvugt | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvule | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvult | SMTLib2.BitVector |
| bvurem | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvxnor | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| bvxor | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| CmdAnnot | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| CmdAssert | SMTLib2.AST, SMTLib2 |
| CmdAssumption | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| CmdCheckSat | SMTLib2.AST, SMTLib2 |
| CmdDeclareFun | SMTLib2.AST, SMTLib2 |
| CmdDeclareType | SMTLib2.AST, SMTLib2 |
| CmdDefineFun | SMTLib2.AST, SMTLib2 |
| CmdDefineType | SMTLib2.AST, SMTLib2 |
| CmdExit | SMTLib2.AST, SMTLib2 |
| CmdExtraFuns | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| CmdExtraPreds | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| CmdExtraSorts | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| CmdFormula | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| CmdGetAssertions | SMTLib2.AST, SMTLib2 |
| CmdGetInfo | SMTLib2.AST, SMTLib2 |
| CmdGetOption | SMTLib2.AST, SMTLib2 |
| CmdGetProof | SMTLib2.AST, SMTLib2 |
| CmdGetUnsatCore | SMTLib2.AST, SMTLib2 |
| CmdGetValue | SMTLib2.AST, SMTLib2 |
| CmdLogic | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| CmdNotes | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| CmdPop | SMTLib2.AST, SMTLib2 |
| CmdPush | SMTLib2.AST, SMTLib2 |
| CmdSetInfo | SMTLib2.AST, SMTLib2 |
| CmdSetLogic | SMTLib2.AST, SMTLib2 |
| CmdSetOption | SMTLib2.AST, SMTLib2 |
| CmdStatus | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Command | |
| 1 (Type/Class) | SMTLib2.AST, SMTLib2 |
| 2 (Type/Class) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| command | SMTLib2.Compat1 |
| concat | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Conn | |
| 1 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| 2 (Type/Class) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| constDef | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| defExpr | SMTLib2.AST, SMTLib2 |
| Defn | |
| 1 (Type/Class) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| defVar | SMTLib2.AST, SMTLib2 |
| err | SMTLib2.Compat1 |
| Exists | |
| 1 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Expr | SMTLib2.AST, SMTLib2 |
| extract | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Fail | SMTLib2.Compat1 |
| false | SMTLib2.Core |
| FAnnot | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| FFalse | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| FLet | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Forall | |
| 1 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Formula | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| formula | SMTLib2.Compat1 |
| FPred | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| FTrue | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| funAnnots | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| funArgs | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| FunDecl | |
| 1 (Type/Class) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| 2 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| funDef | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| funName | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| funRes | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| FVar | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| goal | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| I | |
| 1 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Ident | |
| 1 (Type/Class) | SMTLib2.AST, SMTLib2 |
| 2 (Type/Class) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| ident | SMTLib2.Compat1 |
| Iff | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| IfThenElse | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Implies | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| InfoAllStatistics | SMTLib2.AST, SMTLib2 |
| InfoAttr | SMTLib2.AST, SMTLib2 |
| InfoAuthors | SMTLib2.AST, SMTLib2 |
| InfoErrorBehavior | SMTLib2.AST, SMTLib2 |
| InfoFlag | SMTLib2.AST, SMTLib2 |
| InfoName | SMTLib2.AST, SMTLib2 |
| InfoReasonUnknown | SMTLib2.AST, SMTLib2 |
| InfoStatus | SMTLib2.AST, SMTLib2 |
| InfoVersion | SMTLib2.AST, SMTLib2 |
| isBitVec | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| ITE | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| ite | SMTLib2.Core |
| Let | |
| 1 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Lit | |
| 1 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| LitBV | SMTLib2.AST, SMTLib2 |
| Literal | |
| 1 (Type/Class) | SMTLib2.AST, SMTLib2 |
| 2 (Type/Class) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| literal | SMTLib2.Compat1 |
| LitFrac | |
| 1 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| LitNum | |
| 1 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| LitStr | |
| 1 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| logic | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| N | |
| 1 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Name | |
| 1 (Type/Class) | SMTLib2.AST, SMTLib2 |
| 2 (Type/Class) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| name | SMTLib2.Compat1 |
| Not | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| not | SMTLib2.Core |
| OK | SMTLib2.Compat1 |
| OptAttr | SMTLib2.AST, SMTLib2 |
| OptDiagnosticOutputChannel | SMTLib2.AST, SMTLib2 |
| OptExpandDefinitions | SMTLib2.AST, SMTLib2 |
| OptInteractiveMode | SMTLib2.AST, SMTLib2 |
| Option | SMTLib2.AST, SMTLib2 |
| OptPrintSuccess | SMTLib2.AST, SMTLib2 |
| OptProduceAssignments | SMTLib2.AST, SMTLib2 |
| OptProduceModels | SMTLib2.AST, SMTLib2 |
| OptProduceProofs | SMTLib2.AST, SMTLib2 |
| OptProduceUnsatCores | SMTLib2.AST, SMTLib2 |
| OptRandomSeed | SMTLib2.AST, SMTLib2 |
| OptRegularOutputChannel | SMTLib2.AST, SMTLib2 |
| OptVerbosity | SMTLib2.AST, SMTLib2 |
| Or | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| or | SMTLib2.Core |
| PP | |
| 1 (Type/Class) | SMTLib2.PP, SMTLib2 |
| 2 (Type/Class) | SMTLib1.PP, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| pp | |
| 1 (Function) | SMTLib2.PP, SMTLib2 |
| 2 (Function) | SMTLib1.PP, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| ppString | SMTLib2.PP, SMTLib2 |
| predAnnots | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| predArgs | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| PredDecl | |
| 1 (Type/Class) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| 2 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| predName | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Quant | |
| 1 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 2 (Type/Class) | SMTLib2.AST, SMTLib2 |
| 3 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| 4 (Type/Class) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| quant | SMTLib2.Compat1 |
| repeat | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| rotate_left | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| rotate_right | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Sat | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| scrCommands | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Script | |
| 1 (Type/Class) | SMTLib2.AST, SMTLib2 |
| 2 (Data Constructor) | SMTLib2.AST, SMTLib2 |
| 3 (Type/Class) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| 4 (Data Constructor) | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| script | SMTLib2.Compat1 |
| scrName | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| select | |
| 1 (Function) | SMTLib2.Array |
| 2 (Function) | SMTLib1.QF_AUFBV |
| sign_extend | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Sort | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| sort | SMTLib2.Compat1 |
| Status | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| store | |
| 1 (Function) | SMTLib2.Array |
| 2 (Function) | SMTLib1.QF_AUFBV |
| TAnnot | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| TApp | SMTLib2.AST, SMTLib2 |
| tArray | |
| 1 (Function) | SMTLib2.Array |
| 2 (Function) | SMTLib1.QF_AUFBV |
| tBitVec | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| tBool | SMTLib2.Core |
| Term | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| term | SMTLib2.Compat1 |
| tInt | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| toEither | SMTLib2.Compat1 |
| toMaybe | SMTLib2.Compat1 |
| Trans | SMTLib2.Compat1 |
| true | SMTLib2.Core |
| TVar | SMTLib2.AST, SMTLib2 |
| Type | SMTLib2.AST, SMTLib2 |
| Unknown | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Unsat | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Var | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| Xor | SMTLib1.AST, SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV |
| xor | SMTLib2.Core |
| zero_extend | |
| 1 (Function) | SMTLib2.BitVector |
| 2 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV |