Revise the guide: Rosette Essentials, sections 3.4.0-3.4.2.

sorawee · Jan 29, 2021 · 9348350 · 9348350
1 parent 7f8cc7e
commit 9348350
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/rosette/guide/scribble/essentials/essentials.scrbl b/rosette/guide/scribble/essentials/essentials.scrbl
@@ -431,7 +431,7 @@ But this approximation comes with a downside. Because it is unsound, queries may
 (code:line (time (verify (check-mid-slow bvmid l h))) (code:comment "Loss of soundness!"))]    
 
 
-Navigating this tradeoff between performance and soundness can be tricky. So, when possible, it is best to set @racket[current-bitwidth] to @racket[#f] and limit the use of integers to code that will be evaluated concretely. This approach works well with solvers that reject queries with integers (e.g., @racket[boolector]), so if any make it into a query, the solver fails fast:
+Navigating this tradeoff between performance and soundness can be tricky. So, when possible, it is best to set @racket[current-bitwidth] to @racket[#f] and limit the use of integers to code that will be evaluated concretely. This approach works well with solvers that reject queries over symbolic integers (e.g., @racket[boolector]), so if any have made it into a query, the solver fails fast:
 @interaction[#:eval rosette-eval
 (current-bitwidth #f)
 (require rosette/solver/smt/boolector)