Fix global negate (#2449)

diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index ddebf961f8d0d5eb7d6d2e956a20be4775156742..ae71b3e789fc6c92764a257d9222e2ea8038964d 100644 (file)
--- a/src/preprocessing/passes/global_negate.cpp
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -105,9 +105,15 @@ PreprocessingPassResult GlobalNegate::applyInternal(
   Node trueNode = nm->mkConst(true);
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
   {
-    assertionsToPreprocess->replace(i, trueNode);
+    if (i == 0)
+    {
+      assertionsToPreprocess->replace(i, simplifiedNode);
+    }
+    else
+    {
+      assertionsToPreprocess->replace(i, trueNode);
+    }
   }
-  assertionsToPreprocess->push_back(simplifiedNode);
   return PreprocessingPassResult::NO_CONFLICT;
 }
 

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 59a5b5f64737b9464bd6bfac87c27dc1d385407e..ff6bc1d4e04d1d0316c7309900414b56b7703343 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1672,6 +1672,7 @@ REG2_TESTS = \
        regress2/piVC_5581bd.smt2 \
        regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 \
        regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 \
+       regress2/quantifiers/gn-wrong-091018.smt2 \
        regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 \
        regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 \
        regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 \

diff --git a/test/regress/regress2/quantifiers/gn-wrong-091018.smt2 b/test/regress/regress2/quantifiers/gn-wrong-091018.smt2
new file mode 100644 (file)
index 0000000..733180f
--- /dev/null
+++ b/test/regress/regress2/quantifiers/gn-wrong-091018.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --global-negate --no-check-models
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic BV)
+(set-info :status sat)
+(declare-fun v () (_ BitVec 32))
+(declare-fun g () (_ BitVec 32))
+(declare-fun t () (_ BitVec 32))
+(declare-fun V () (_ BitVec 32))
+(declare-fun vuscore2dollarskuscore0 () (_ BitVec 32))
+(declare-fun huscore2dollarskuscore0 () (_ BitVec 32))
+(declare-fun c () (_ BitVec 32))
+(declare-fun t1uscore0dollarskuscore0 () (_ BitVec 32))
+(declare-fun tuscore2dollarskuscore0 () (_ BitVec 32))
+(declare-fun ts1uscore0 () (_ BitVec 32))
+(declare-fun h () (_ BitVec 32))
+(assert (not (exists ((ts1uscore0 (_ BitVec 32))) (let ((?v_2 (bvmul (_ bv2 32) huscore2dollarskuscore0)) (?v_0 (bvsdiv g (_ bv2 32))) (?v_1 (bvneg g)) (?v_4 (bvadd t1uscore0dollarskuscore0 tuscore2dollarskuscore0)) (?v_3 (bvmul (bvneg (_ bv1 32)) g))) (=> (and (and (and (and (and (and (and (and (and (and (and (and (=> (and (bvsle (_ bv0 32) ts1uscore0) (bvsle ts1uscore0 t1uscore0dollarskuscore0)) (bvsge (bvmul (bvsdiv (_ bv1 32) (_ bv2 32)) (bvadd (bvadd ?v_2 (bvmul ?v_3 (bvmul ts1uscore0 ts1uscore0))) (bvmul (bvmul (_ bv2 32) ts1uscore0) vuscore2dollarskuscore0))) (_ bv0 32))) (bvsge t1uscore0dollarskuscore0 (_ bv0 32))) (= huscore2dollarskuscore0 (bvadd (bvmul ?v_0 (bvmul tuscore2dollarskuscore0 tuscore2dollarskuscore0)) (bvmul vuscore2dollarskuscore0 tuscore2dollarskuscore0)))) (bvsge huscore2dollarskuscore0 (_ bv0 32))) (bvsge tuscore2dollarskuscore0 (_ bv0 32))) (bvsle vuscore2dollarskuscore0 (bvadd (bvmul ?v_1 tuscore2dollarskuscore0) V))) (bvsgt g (_ bv0 32))) (bvsle (_ bv0 32) c)) (bvslt c (_ bv1 32))) (= h (bvadd (bvmul ?v_0 (bvmul t t)) (bvmul v t)))) (bvsge h (_ bv0 32))) (bvsge t (_ bv0 32))) (bvsle v (bvadd (bvmul ?v_1 t) V))) (or (bvsgt ?v_4 (_ bv0 32)) (= (bvmul (bvsdiv (_ bv1 32) (_ bv2 32)) (bvadd (bvadd ?v_2 (bvmul ?v_3 (bvmul t1uscore0dollarskuscore0 t1uscore0dollarskuscore0))) (bvmul (bvmul (_ bv2 32) t1uscore0dollarskuscore0) vuscore2dollarskuscore0))) (bvadd (bvmul ?v_0 (bvmul ?v_4 ?v_4)) (bvmul (bvadd (bvmul ?v_3 t1uscore0dollarskuscore0) vuscore2dollarskuscore0) ?v_4)))))))))
+(check-sat)
+(exit)