| r | Documentation.SBV.Examples.WeakestPreconditions.IntDiv | 
| RandomSeed | Data.SBV.Trans.Control, Data.SBV.Control | 
| Range |  | 
| 1 (Data Constructor) | Data.SBV.RegExp, Data.SBV.Internals | 
| 2 (Type/Class) | Data.SBV.Tools.Range | 
| 3 (Data Constructor) | Data.SBV.Tools.Range | 
| ranges | Data.SBV.Tools.Range | 
| rangesWith | Data.SBV.Tools.Range | 
| RatApprox | Data.SBV | 
| RatExact | Data.SBV | 
| RatInterval | Data.SBV | 
| Ratio | Data.SBV.Trans, Data.SBV | 
| Rational | Data.SBV.Trans, Data.SBV | 
| RationalConstructor | Data.SBV.Internals | 
| RationalCV | Data.SBV | 
| RatIrreducible | Data.SBV | 
| RC4 | Documentation.SBV.Examples.Crypto.RC4 | 
| rc4IsCorrect | Documentation.SBV.Examples.Crypto.RC4 | 
| RCSet | Data.SBV.Internals, Data.SBV | 
| readArray | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| readBin | Data.SBV.Internals | 
| readSArr | Data.SBV.Dynamic | 
| readSTree | Data.SBV.Tools.STree | 
| ReadVar | Documentation.SBV.Examples.Strings.SQLInjection | 
| Ready | Documentation.SBV.Examples.Lists.BoundedMutex | 
| RealPoint | Data.SBV | 
| realPoint | Data.SBV | 
| ReasonUnknown | Data.SBV.Trans.Control, Data.SBV.Control | 
| Red |  | 
| 1 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Fish | 
| 2 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Garden | 
| 3 (Data Constructor) | Documentation.SBV.Examples.Puzzles.HexPuzzle | 
| redirectVerbose | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| RegA | Documentation.SBV.Examples.BitPrecise.Legato | 
| RegExp | Data.SBV.RegExp, Data.SBV.Internals | 
| RegExpMatchable | Data.SBV.RegExp | 
| Register | Documentation.SBV.Examples.BitPrecise.Legato | 
| registerKind | Data.SBV.Internals | 
| Registers | Documentation.SBV.Examples.BitPrecise.Legato | 
| registers | Documentation.SBV.Examples.BitPrecise.Legato | 
| registerUISMTFunction | Data.SBV.Control | 
| RegularCV | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| RegularSet | Data.SBV.Internals, Data.SBV | 
| RegX | Documentation.SBV.Examples.BitPrecise.Legato | 
| Rem | Data.SBV.Internals | 
| renderCgPgmBundle | Data.SBV.Internals | 
| renderTest | Data.SBV.Tools.GenTest | 
| replace |  | 
| 1 (Function) | Data.SBV.String | 
| 2 (Function) | Data.SBV.List | 
| ReproducibleResourceLimit | Data.SBV.Trans.Control, Data.SBV.Control | 
| resArrays | Data.SBV.Internals | 
| resAsgns | Data.SBV.Internals | 
| resAssertions | Data.SBV.Internals | 
| resAxioms | Data.SBV.Internals | 
| resConstraints | Data.SBV.Internals | 
| resConsts | Data.SBV.Internals | 
| resetAssertions |  | 
| 1 (Function) | Data.SBV.Trans.Control | 
| 2 (Function) | Data.SBV.Control | 
| resInputs | Data.SBV.Internals | 
| reskinds | Data.SBV.Internals | 
| resObservables | Data.SBV.Internals | 
| resOutputs | Data.SBV.Internals | 
| Resp_AllStatistics | Data.SBV.Trans.Control, Data.SBV.Control | 
| Resp_AssertionStackLevels | Data.SBV.Trans.Control, Data.SBV.Control | 
| Resp_Authors | Data.SBV.Trans.Control, Data.SBV.Control | 
| Resp_Error | Data.SBV.Trans.Control, Data.SBV.Control | 
| Resp_InfoKeyword | Data.SBV.Trans.Control, Data.SBV.Control | 
| Resp_Name | Data.SBV.Trans.Control, Data.SBV.Control | 
| Resp_ReasonUnknown | Data.SBV.Trans.Control, Data.SBV.Control | 
| Resp_Unsupported | Data.SBV.Trans.Control, Data.SBV.Control | 
| Resp_Version | Data.SBV.Trans.Control, Data.SBV.Control | 
| resTables | Data.SBV.Internals | 
| resTraces | Data.SBV.Internals | 
| resUIConsts | Data.SBV.Internals | 
| resUISegs | Data.SBV.Internals | 
| Result |  | 
| 1 (Type/Class) | Data.SBV.Internals | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| 3 (Type/Class) | Documentation.SBV.Examples.Transformers.SymbolicEval | 
| 4 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval | 
| result | Documentation.SBV.Examples.Transformers.SymbolicEval | 
| retrieveResponseFromSolver | Data.SBV.Internals | 
| Rol | Data.SBV.Internals | 
| Role | Documentation.SBV.Examples.Puzzles.Murder | 
| role | Documentation.SBV.Examples.Puzzles.Murder | 
| Ror | Data.SBV.Internals | 
| rorM | Documentation.SBV.Examples.BitPrecise.Legato | 
| rorR | Documentation.SBV.Examples.BitPrecise.Legato | 
| rotate | Data.SBV.Trans, Data.SBV | 
| rotateL | Data.SBV.Trans, Data.SBV | 
| rotateR | Data.SBV.Trans, Data.SBV | 
| rotR | Documentation.SBV.Examples.Crypto.AES | 
| roundConstants | Documentation.SBV.Examples.Crypto.AES | 
| roundingAdd | Documentation.SBV.Examples.Misc.Floating | 
| RoundingMode | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| roundingMode | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| RoundNearestTiesToAway | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| RoundNearestTiesToEven | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| RoundTowardNegative | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| RoundTowardPositive | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| RoundTowardZero | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| Row |  | 
| 1 (Type/Class) | Documentation.SBV.Examples.Puzzles.MagicSquare | 
| 2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Sudoku | 
| run | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| runAlloc | Documentation.SBV.Examples.Transformers.SymbolicEval | 
| runEval | Documentation.SBV.Examples.Transformers.SymbolicEval | 
| runLegato | Documentation.SBV.Examples.BitPrecise.Legato | 
| runProgramEval | Documentation.SBV.Examples.Transformers.SymbolicEval | 
| runPropertyEval | Documentation.SBV.Examples.Transformers.SymbolicEval | 
| runQ | Documentation.SBV.Examples.Transformers.SymbolicEval | 
| runQueryT | Data.SBV.Internals | 
| runSMT |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| runSMTWith |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| runSymbolic | Data.SBV.Internals |