summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-09-10 23:31:29 -0500
committerHaniel Barbosa <hanielbbarbosa@gmail.com>2018-09-10 23:31:29 -0500
commitb0c630be79034d898e473c167a16fb61c380b733 (patch)
treebd5913e96365080e300e6eb9792a77b8d6af831d
parent945da3af1ea94aeabcd8f39b23a8741c6e41c358 (diff)
Fix global negate (#2449)
-rw-r--r--src/preprocessing/passes/global_negate.cpp10
-rw-r--r--test/regress/Makefile.tests1
-rw-r--r--test/regress/regress2/quantifiers/gn-wrong-091018.smt219
3 files changed, 28 insertions, 2 deletions
diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index ddebf961f..ae71b3e78 100644
--- 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 59a5b5f64..ff6bc1d4e 100644
--- 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
index 000000000..733180faa
--- /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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback