elim-uncnstr2 unsoudness

[nunoplopes]

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]

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]

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]

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))