diff --git a/doc/sphinx/source/basic-usage.rst b/doc/sphinx/source/basic-usage.rst index 53335240c..f359f37e4 100644 --- a/doc/sphinx/source/basic-usage.rst +++ b/doc/sphinx/source/basic-usage.rst @@ -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 --------------------- @@ -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>`. +