Fix unsound double abs rewrite rule for FP (#2792)

diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 21644161e670f04e6ad4b94fdc36d39dab245c58..875471dedee2ff23224d397ec407ed7431f97eef 100644 (file)
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -76,9 +76,12 @@ namespace rewrite {
 
   RewriteResponse compactAbs (TNode node, bool) {
     Assert(node.getKind() == kind::FLOATINGPOINT_ABS);
-    if (node[0].getKind() == kind::FLOATINGPOINT_NEG ||
-       node[0].getKind() == kind::FLOATINGPOINT_ABS) {
-      return RewriteResponse(REWRITE_AGAIN, node[0][0]);
+    if (node[0].getKind() == kind::FLOATINGPOINT_NEG
+        || node[0].getKind() == kind::FLOATINGPOINT_ABS)
+    {
+      Node ret =
+          NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_ABS, node[0][0]);
+      return RewriteResponse(REWRITE_AGAIN, ret);
     }
 
     return RewriteResponse(REWRITE_DONE, node);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e6e28336ef4529bc9682370a49550244e9d403a3..dbefe3af270ec9c4bf78b53aa6b6790fb98e1b3a 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -444,6 +444,8 @@ set(regress_0_tests
   regress0/fmf/sort-infer-typed-082718.smt2
   regress0/fmf/syn002-si-real-int.smt2
   regress0/fmf/tail_rec.smt2
+  regress0/fp/abs-unsound.smt2
+  regress0/fp/abs-unsound2.smt2
   regress0/fp/ext-rew-test.smt2
   regress0/fp/simple.smt2
   regress0/fuzz_1.smt

diff --git a/test/regress/regress0/fp/abs-unsound.smt2 b/test/regress/regress0/fp/abs-unsound.smt2
new file mode 100644 (file)
index 0000000..4ac53b8
--- /dev/null
+++ b/test/regress/regress0/fp/abs-unsound.smt2
@@ -0,0 +1,11 @@
+; REQUIRES: symfpu
+; EXPECT: sat
+(set-logic QF_FP)
+(set-info :status sat)
+(declare-fun x () (_ FloatingPoint 3 5))
+(declare-fun y () (_ FloatingPoint 3 5))
+
+(assert (not (= (fp.abs (fp.abs x)) x)))
+(assert (not (= (fp.abs (fp.neg y)) y)))
+
+(check-sat)

diff --git a/test/regress/regress0/fp/abs-unsound2.smt2 b/test/regress/regress0/fp/abs-unsound2.smt2
new file mode 100644 (file)
index 0000000..a6172b1
--- /dev/null
+++ b/test/regress/regress0/fp/abs-unsound2.smt2
@@ -0,0 +1,9 @@
+; REQUIRES: symfpu
+; EXPECT: unsat
+(set-logic QF_FP)
+(set-info :status unsat)
+(declare-fun x () (_ FloatingPoint 3 5))
+
+(assert (fp.isNegative (fp.abs (fp.neg x))))
+
+(check-sat)