diff options
| author |  qadeer <unknown> | 2012-02-23 13:57:10 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2012-02-23 13:57:10 -0800 |
| commit | 88a325c862048ab6d487fc8f5d6fcba3602960df (patch) | |
| tree | aac68757ad46345b571fbd3a09358c052be84d7d /Source | |
| parent | dc8e43c41b46e8d2ae9bc93caa97f7b7d891b5df (diff) | |
| parent | c793a5ea9bf33f9f7028af9920e569b5ec7fcc4f (diff) | |
Merge
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibNamer.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index a874c6c5..5629c0d6 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -36,6 +36,12 @@ namespace Microsoft.Boogie.SMTLib "bvsge", "bvslt", "bvugt", "bvsgt", "bvxor", "bvnand", "bvnor", "bvxnor", "sign_extend", "zero_extend",
"repeat", "bvredor", "bvredand", "bvcomp", "bvumul_noovfl", "bvsmul_noovfl", "bvsmul_noudfl", "bvashr",
"rotate_left", "rotate_right", "ext_rotate_left", "ext_rotate_right", "int2bv", "bv2int",
+ // floating point
+ "plusInfinity", "minusInfinity", "NaN",
+ "roundNearestTiesToEven", "roundNearestTiesToAway", "roundTowardPositive", "roundTowardNegative", "roundTowardZero",
+ "+", "-", "/", "*", "==", "<", ">", "<=", ">=",
+ "abs", "remainder", "fusedMA", "squareRoot", "roundToIntegral",
+ "isZero", "isNZero", "isPZero", "isSignMinus", "min", "max", "asFloat",
// SMT v1 stuff
"flet", "implies", "!=", "if_then_else",
// Z3 extensions
|