diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2015-02-18 19:54:02 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-02-18 19:54:02 +0000 |
| commit | 9359c725fed422323d68ce4b4a58b0e4d776064d (patch) | |
| tree | 0d36dbd13ed65d83d43c5ed2fe5862246c7e86c3 | |
| parent | 59fdb656f09cb4f51fc60d30d8c1bef59f5f908d (diff) | |
Fix bug where some reserved Z3 keywords were not sanitized
when generating the VC.
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibNamer.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index 101b07a0..b6a6aafa 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -47,6 +47,7 @@ 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",
};
|