diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2015-02-27 12:09:10 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-02-27 12:09:10 +0000 |
| commit | 7cd4f74474c3935e6d0e67d67e86c6c8326a95a4 (patch) | |
| tree | ba55ad70160d8c679a9fed11191c5284379b2e71 /Source/Provers | |
| parent | aa48ab54832d6301ad0511227dea40df2b959a5f (diff) | |
Fix using reserved Z3 keywords for real/int arithmetic operators. These are taken
from `` arith_decl_plugin::get_op_names(...)`` from ``src/ast/arith_decl_plugin.cpp``
in the Z3 4.3.2 source code.
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibNamer.cs | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index 502e89e5..8e000403 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -23,7 +23,9 @@ namespace Microsoft.Boogie.SMTLib "and", "or", "not", "iff", "true", "false", "xor", "distinct", "ite", "=", "Bool",
"=>", // implies (sic!)
// Integers and reals
- "Int", "Real", "*", "/", "-", "+", "<", "<=", ">", ">=", "div", "mod",
+ "Int", "Real", "*", "/", "-", "~", "+", "<", "<=", ">", ">=", "div", "mod", "rem",
+ "^", "sin", "cos", "tan", "asin", "acos", "atan", "sinh", "cosh", "tanh", "asinh", "acosh", "atanh", "pi", "euler",
+ "to_real", "to_int", "is_int",
// Bitvectors
"extract", "concat",
"bvnot", "bvneg", "bvand", "bvor", "bvadd", "bvmul", "bvudiv", "bvurem", "bvshl", "bvlshr", "bvult",
@@ -46,7 +48,6 @@ namespace Microsoft.Boogie.SMTLib // Z3 extensions
"lblneg", "lblpos", "lbl-lit",
"if", "&&", "||", "equals", "equiv", "bool",
- "sin", "cos", "tan", "asin", "acos", "atan",
// Boogie-defined
"real_pow", "UOrdering2", "UOrdering3",
// Floating point (final draft SMTLIB-v2.5)
|