Skip to content

Commit

Permalink
More detail in the documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
@gussmith23
gussmith23 committed Dec 14, 2023
1 parent c4eacea commit 44f4c3c
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions rosette/guide/scribble/datatypes/solvers+solutions.scrbl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -400,8 +400,9 @@ executable as the optional @racket[path] argument.
Rosette specifically uses the @tt{yices-smt2} executable, which is the Yices2
solver with its SMTLIB2 frontend enabled.
Note that just building (without installing) Yices2 will produce an executable
named @tt{yices_smt2}. This executable can safely be renamed or symlinked to
@tt{yices-smt2}.
named @tt{yices_smt2}. Running the installation step produces an executable
with the correct name. However, it is safe to skip the installation step and
simply rename or symlink the @tt{yices_smt2} executable to @tt{yices-smt2}.
Rosette currently tests Yices2 at commit
@tt{e27cf308cffb0ecc6cc7165c10e81ca65bc303b3}.

Expand Down

0 comments on commit 44f4c3c

Please sign in to comment.