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 |