From c793a5ea9bf33f9f7028af9920e569b5ec7fcc4f Mon Sep 17 00:00:00 2001 From: qadeer Date: Mon, 20 Feb 2012 14:59:04 -0800 Subject: added floating point keywords to reserved SMTwords list --- Source/Provers/SMTLib/SMTLibNamer.cs | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'Source/Provers/SMTLib') 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 -- cgit v1.2.3