From c6f4cdab0f0b47759c5e686462fd09449de90a0d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 May 2013 17:49:03 -0700 Subject: [PATCH] Fix bug reported at https://z3.codeplex.com/workitem/41 Signed-off-by: Leonardo de Moura --- src/ast/pattern/database.smt2 | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/pattern/database.smt2 b/src/ast/pattern/database.smt2 index 9021e44f0..c42c9c25f 100644 --- a/src/ast/pattern/database.smt2 +++ b/src/ast/pattern/database.smt2 @@ -119,13 +119,13 @@ :pattern (?select (?select (?asElems e) a) i)))) (assert (forall ((x Int) (f Int) (a0 Int)) (! - (or (<= (+ a0 (* -1 (?fClosedTime f))) 0) + (or (<= (+ a0 (* (- 1) (?fClosedTime f))) 0) (not (= (?isAllocated x a0) 1)) (= (?isAllocated (?select f x) a0) 1)) :pattern (?isAllocated (?select f x) a0)))) (assert (forall ((a Int) (e Int) (i Int) (a0 Int)) (! - (or (<= (+ a0 (* -1 (?eClosedTime e))) 0) + (or (<= (+ a0 (* (- 1) (?eClosedTime e))) 0) (not (= (?isAllocated a a0) 1)) (= (?isAllocated (?select (?select e a) i) a0) 1)) :pattern (?isAllocated (?select (?select e a) i) a0)))) @@ -281,13 +281,13 @@ :pattern (IntsAllocated h (?StructGet_ s f))))) (assert (forall ((x Int) (f Int) (a0 Int)) (! - (or (<= (+ a0 (* -1 (?fClosedTime f))) 0) + (or (<= (+ a0 (* (- 1) (?fClosedTime f))) 0) (not (?isAllocated_ x a0)) (?isAllocated_ (?select f x) a0)) :pattern (?isAllocated_ (?select f x) a0)))) (assert (forall ((a Int) (e Int) (i Int) (a0 Int)) (! - (or (<= (+ a0 (* -1 (?eClosedTime e))) 0) + (or (<= (+ a0 (* (- 1) (?eClosedTime e))) 0) (not (?isAllocated_ a a0)) (?isAllocated_ (?select (?select e a) i) a0)) :pattern (?isAllocated_ (?select (?select e a) i) a0))))