Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

elim-uncnstr2 unsoudness #6488

Closed
nunoplopes opened this issue Dec 12, 2022 · 3 comments
Closed

elim-uncnstr2 unsoudness #6488

nunoplopes opened this issue Dec 12, 2022 · 3 comments

Comments

@nunoplopes
Copy link
Collaborator

So we don't forget, here's a bug handling bvule:

(declare-fun %p () (_ BitVec 5))
(declare-fun init_mem_1 () (Array (_ BitVec 2) (_ BitVec 34)))
(declare-fun undef!14 () (_ BitVec 32))

(assert (forall ((undef!5 (_ BitVec 32)))
          (and (= ((_ extract 33 33) (select init_mem_1 ((_ extract 3 2) %p))) #b1)
               (bvule ((_ extract 31 0) (select init_mem_1 ((_ extract 3 2) %p))) undef!5)
               (not (bvule ((_ extract 31 0) (select init_mem_1 ((_ extract 3 2) %p))) undef!14)))))

(check-sat-using (then elim-uncnstr smt))
(check-sat-using (then elim-uncnstr2 smt))
@nunoplopes
Copy link
Collaborator Author

new crash:

(declare-fun isundef_%i () (_ BitVec 1))
(declare-fun isundef_%p () (_ BitVec 1))
(declare-fun |#undef'!16| () (_ BitVec 32))
(declare-fun %p () (_ BitVec 5))
(declare-fun init_mem_1 () (Array (_ BitVec 2) (_ BitVec 34)))
(declare-fun blk_align_tgt ((_ BitVec 1)) (_ BitVec 6))

(assert (let ((a!3 (forall ((undef!4 (_ BitVec 4)))
                (bvule #b000011 (blk_align_tgt ((_ extract 4 4) %p)))))
      (a!4 (forall ((undef!10 (_ BitVec 32)))
                      (bvule ((_ extract 31 0) (select init_mem_1 ((_ extract 3 2) %p)))
                                   (bvadd #x00000007 |#undef'!16|)))))
       (or (and a!3 (= #b0 isundef_%p) (= #b0 isundef_%i))
           (and a!4 (= #b0 isundef_%p) (= isundef_%i #b1)))))

(check-sat-using (then simplify propagate-values simplify elim-uncnstr2 qe-light simplify elim-uncnstr2))
(check-sat-using (then simplify propagate-values simplify elim-uncnstr2 qe-light simplify elim-uncnstr2 reduce-args qe-light simplify smt))

@nunoplopes nunoplopes reopened this Dec 12, 2022
@nunoplopes
Copy link
Collaborator Author

Another crash, sorry:

(declare-fun |isundef_%y#1| () (_ BitVec 1))
(declare-fun |isundef_%y#0| () (_ BitVec 1))
(declare-fun |isundef_%x#1| () (_ BitVec 1))
(declare-fun |isundef_%x#0| () (_ BitVec 1))
(declare-fun undef!8 () (_ BitVec 4))
(declare-fun undef!10 () (_ BitVec 4))
(declare-fun |np_%y#1| () Bool)
(declare-fun undef!7 () (_ BitVec 4))
(declare-fun undef!6 () (_ BitVec 4))
(declare-fun undef!9 () (_ BitVec 4))
(declare-fun |np_%y#0| () Bool)
(declare-fun |np_%x#1| () Bool)
(declare-fun |np_%x#0| () Bool)
(declare-fun |%x#1| () (_ BitVec 4))
(declare-fun |%y#0| () (_ BitVec 4))
(declare-fun |%x#0| () (_ BitVec 4))
(declare-fun |%y#1| () (_ BitVec 4))

(assert (let ((a!1 (forall ((undef!0 (_ BitVec 4))
                    (undef!1 (_ BitVec 4))
                    (undef!4 (_ BitVec 4)))
             (! (let ((a!1 (or (not |np_%y#0|)
                               (= (bvule |%y#0| (bvudiv_i undef!0 undef!1))
                                  (bvule |%y#0| (bvudiv_i undef!6 undef!7))))))
                  (and |np_%x#0|
                       (not a!1)))
                :weight 0)))
      (a!2 (and (and (= |isundef_%x#0| #b1) (= #b0 |isundef_%x#1|))
                (= #b0 |isundef_%y#0|)))
      (a!8 (forall ((undef!0 (_ BitVec 4))
                    (undef!1 (_ BitVec 4))
                    (undef!2 (_ BitVec 4))
                    (undef!3 (_ BitVec 4))
                    (undef!4 (_ BitVec 4)))
             (! (let ((a!1 (or (not |np_%y#0|)
                               (= (bvule undef!3 (bvudiv_i undef!0 |%x#0|))
                                  (bvule undef!9 (bvudiv_i undef!6 |%x#0|)))))
                      (a!2 (or (not |np_%y#1|)
                               (= (bvule undef!4 (bvudiv_i #xf undef!2))
                                  (bvule undef!10 (bvudiv_i #xf undef!8))))))
                  (and |np_%x#0|
                       (not (= undef!2 #x0))
                       (not (= undef!8 #x0))
                       (not (and a!1 a!2))))
                :weight 0)))
      (a!9 (and (and (= #b0 |isundef_%x#0|) (= |isundef_%x#1| #b1))
                (= |isundef_%y#0| #b1)))
      (a!18 (and (and (= #b0 |isundef_%x#0|) (= #b0 |isundef_%x#1|))
                 (= #b0 |isundef_%y#0|)))
      (a!19 (forall ((undef!0 (_ BitVec 4))
                     (undef!1 (_ BitVec 4))
                     (undef!2 (_ BitVec 4))
                     (undef!3 (_ BitVec 4))
                     (undef!4 (_ BitVec 4)))
              (! (let ((a!1 (or (not |np_%y#0|)
                                (= (bvule undef!3 (bvudiv_i undef!0 |%x#0|))
                                   (bvule undef!9 (bvudiv_i undef!6 |%x#0|)))))
                       (a!2 (or (not |np_%y#1|)
                                (= (bvule undef!4 (bvudiv_i #xf |%x#1|))
                                   (bvule undef!10 (bvudiv_i #xf |%x#1|))))))
                   (and |np_%x#0|
                        |np_%x#1|
                        (not (= |%x#0| #x0))
                        (not (= |%x#1| #x0))
                        (not (and a!1 a!2))))
                 :weight 0)))
      (a!22 (forall ((undef!0 (_ BitVec 4))
                     (undef!1 (_ BitVec 4))
                     (undef!2 (_ BitVec 4))
                     (undef!3 (_ BitVec 4))
                     (undef!4 (_ BitVec 4)))
              (! (let ((a!1 (or (not |np_%y#0|)
                                (= (bvule |%y#0| (bvudiv_i undef!0 |%x#0|))
                                   (bvule |%y#0| (bvudiv_i undef!6 |%x#0|))))))
                   (and |np_%x#0|
                        |np_%x#1|
                        (not (= |%x#0| #x0))
                        (not a!1)))
                 :weight 0)))
      (a!24 (forall ((undef!0 (_ BitVec 4))
                     (undef!1 (_ BitVec 4))
                     (undef!2 (_ BitVec 4))
                     (undef!3 (_ BitVec 4))
                     (undef!4 (_ BitVec 4)))
              (! (let ((a!1 (or (not |np_%y#0|)
                                (= (bvule undef!3 (bvudiv_i undef!0 undef!1))
                                   (bvule undef!9 (bvudiv_i undef!6 undef!7)))))
                       (a!2 (or (not |np_%y#1|)
                                (= (bvule undef!4 (bvudiv_i #xf undef!2))
                                   (bvule undef!10 (bvudiv_i #xf undef!8))))))
                   (and
                        (not (= undef!2 #x0))
                        (not (and a!1 a!2))))))))
  (or (and a!2 (= #b0 |isundef_%y#1|))
      (and a!9 a!8 (= |isundef_%y#1| #b1))
      (and a!19 (= |isundef_%y#1| #b1))
      (and a!18 (= #b0 |isundef_%y#1|))
      (and a!24 (= |isundef_%y#1| #b1)))))

(check-sat-using (then simplify propagate-values simplify elim-uncnstr2 qe-light simplify elim-uncnstr2))

@nunoplopes nunoplopes reopened this Dec 12, 2022
@nunoplopes
Copy link
Collaborator Author

Yet another crash:

(declare-fun undef!6 () (_ BitVec 32))
(declare-fun %best_len () (_ BitVec 32))
(declare-fun isundef_%best_len () (_ BitVec 1))
(declare-fun %win () (_ BitVec 66))
(declare-fun undef!5 () (_ BitVec 32))
(declare-fun %cur_match () (_ BitVec 32))
(declare-fun isundef_%cur_match () (_ BitVec 1))
(declare-fun init_mem_1 () (Array (_ BitVec 62) (_ BitVec 34)))
(declare-fun init_mem_2 () (Array (_ BitVec 62) (_ BitVec 34)))
(declare-fun undef!7 () (_ BitVec 32))
(declare-fun %scan_end () (_ BitVec 32))
(declare-fun isundef_%scan_end () (_ BitVec 1))
(declare-fun undef!9 () (_ BitVec 32))
(declare-fun %limit () (_ BitVec 32))
(declare-fun isundef_%limit () (_ BitVec 1))
(declare-fun undef!20 () (_ BitVec 32))
(declare-fun undef!12 () (_ BitVec 32))
(declare-fun %wmask () (_ BitVec 32))
(declare-fun isundef_%wmask () (_ BitVec 1))
(declare-fun %prev () (_ BitVec 66))
(declare-fun undef!39 () (_ BitVec 32))
(declare-fun undef!31 () (_ BitVec 32))
(declare-fun undef!30 () (_ BitVec 32))
(declare-fun %match () (_ BitVec 66))

(assert (let ((a!10 (concat #b000000000000000000000000000000
                    (bvand (ite (= #b0 isundef_%wmask) %wmask undef!30)
                           (ite (= #b0 isundef_%cur_match) %cur_match undef!31))))
      (a!17 (concat #b000000000000000000000000000000
                    (bvand (ite (= #b0 isundef_%wmask) %wmask undef!12)
                           (ite (= #b0 isundef_%cur_match) %cur_match undef!20))))
      (a!22 (bvadd (concat #x00000000 (ite (= #b0 isundef_%cur_match) %cur_match undef!5))
                   (concat #x00000000 (ite (= #b0 isundef_%best_len) %best_len undef!6)))))
(let ((a!11 (select init_mem_2 ((_ extract 63 2) (bvadd ((_ extract 63 0) %prev) (concat a!10 #b00)))))
      (a!18 (select init_mem_2 ((_ extract 63 2) (bvadd ((_ extract 63 0) %prev) (concat a!17 #b00)))))
      (a!23 (ite (= ((_ extract 65 64) %win) #b11)
                 (select init_mem_1 ((_ extract 63 2) a!22))
                 (ite (= #b10 ((_ extract 65 64) %win))
                      (select init_mem_2 ((_ extract 63 2) a!22))
                      (select init_mem_1 ((_ extract 63 2) a!22))))))
(let ((a!13 ((_ extract 31 0) (ite (= ((_ extract 65 64) %prev) #b10) a!11 a!11)))
      (a!20 ((_ extract 31 0) (ite (= ((_ extract 65 64) %prev) #b10) a!18 a!18)))
      (a!24 (= (ite (= #b0 isundef_%scan_end) %scan_end undef!7) ((_ extract 31 0) a!23))))
(let ((a!14 (concat #x00000000 a!13))
      (a!21 (bvule a!20 (ite (= #b0 isundef_%limit) %limit undef!9))))
(let ((a!16 (= ((_ extract 31 0) (select init_mem_1 ((_ extract 63 2) a!14)))
               (ite (= #b0 isundef_%scan_end) %scan_end undef!39))))
  (and (bvule ((_ extract 65 64) %match) #b01)
       (and a!16 a!21 a!24))))))))

(check-sat-using (then elim-uncnstr smt))
(check-sat-using (then elim-uncnstr2 smt))

@nunoplopes nunoplopes reopened this Dec 13, 2022
hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023
@NikolajBjorner @hgvk94
fix Z3Prover#6488
02d9947
hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023
@NikolajBjorner @hgvk94
fix Z3Prover#6488
29520a1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023
@NikolajBjorner @hgvk94
fix Z3Prover#6488
7fc614f 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023
@NikolajBjorner @hgvk94
fix Z3Prover#6488
1367ecd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@nunoplopes