Skip to content

Commit

Permalink
Edits to the doc
Browse files Browse the repository at this point in the history
  • Loading branch information
BrunoDutertre committed Feb 3, 2017
1 parent 473d649 commit 385fbe6
Showing 1 changed file with 15 additions and 14 deletions.
29 changes: 15 additions & 14 deletions doc/sphinx/source/basic-usage.rst
Original file line number Diff line number Diff line change
Expand Up @@ -16,20 +16,6 @@ to initialize Yices, construct and print terms, create a context and
assert formulas, and build and query a model when a context is
satisfiable.

.. warning::

You may encounter problems if you compile the example with Visual
Studio on Windows. These problems are caused by incompatibilities
between C runtime libraries of Visual Studio and the one Yices is
linked against. See https://msdn.microsoft.com/en-us/library/ms235460(v=vs.140).aspx
for a detailed explanation.

To avoid these issues, we recommend compiling with mingw.
It is still possible to use Visual Studio or other compilers on Windows,
as long as you avoid functions in the Yices API that take a :c:type:`FILE *`
argument. File :file:`examples/example1b.c` in the distribution shows
how to use alternative functions for pretty printing.


Global Initialization
---------------------
Expand Down Expand Up @@ -267,3 +253,18 @@ Running this example should produce something like this:
Value of y = 100
.. warning::

You may encounter problems if you compile the example with Visual
Studio on Windows. These problems are caused by incompatibilities
between C runtime libraries of Visual Studio and the one Yices is
linked against. See https://msdn.microsoft.com/en-us/library/ms235460(v=vs.140).aspx
for a detailed explanation.

To avoid these issues, we recommend compiling with mingw.
It is still possible to use Visual Studio or other compilers on Windows,
as long as you avoid functions in the Yices API that take a :c:type:`FILE *`
argument. File :file:`examples/example1b.c` in the distribution shows
how to use alternative functions for pretty printing. You can also
download this file :download:`here <_static/example1b.c>`.

0 comments on commit 385fbe6

Please sign in to comment.