Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:smt-lib_format [2008/03/06 17:56]
vkuncak created
sav08:smt-lib_format [2015/04/21 17:30] (current)
Line 1: Line 1:
 ====== SMT-LIB Format ====== ====== SMT-LIB Format ======
  
-Here [[http://​combination.cs.uiowa.edu/​smtlib/​|official SMT-LIB page]].+Here is the [[http://​combination.cs.uiowa.edu/​smtlib/​|official SMT-LIB page]].
  
 To check satisfiability of formula To check satisfiability of formula
-\[+\begin{equation*}
    (x = 2 \land x < y \land y < 0) \lor (x = y \land x < 3 \land 4 < y)    (x = 2 \land x < y \land y < 0) \lor (x = y \land x < 3 \land 4 < y)
-\]+\end{equation*}
 you can write the following file in SMT-LIB format: you can write the following file in SMT-LIB format:
 <​code>​ <​code>​
 
sav08/smt-lib_format.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice