kooshan commented 8 years ago

Hi, I'm using CBMC (CPROVER tools) to translate some (floating point variables involved) C programs to smtlib2 format and perform some analysis on them using Z3. I've got two sets of variables, non-deterministic (input) variables and some random (output) variables. I need to count atomic predicates which random outputs participate in and then forge a closure of non-deterministic variables involved in those predicates. The problem is, when i use "Z3_parse_smtlib2_string" function to parse the CBMC output and setup the basis formula in a z3 context and solver, the parser righteously simplifies and rules out some of my random outputs to bare literals. in some cases, it's extreme enough that the final formula lacks neither any kind of random output nor atomic predicates in which random outputs could participate. I'm completely a newbie to Z3, and it's C/C++ API. I wanted to ask if there is a workaround to disable such simplification of variables to literals while parsing. I would also appreciate any other idea than writing my own parser for directly analyzing smtlib2 file from CBMC. Thanks in advance.

kooshan commented 8 years ago

to elaborate on my issue please consider this simple program:

int main(void){ float S; //@rvar(HI)[0-6] float Output; //@ivar(LO)[0-6] if (S == 0.0) Output = 0.0; else if (S == 1.0) Output = 1.0; else if (S == 2.0) Output = 2.0; else if (S == 3.0) Output = 3.0; else if (S == 4.0) Output = 4.0; else if (S == 5.0) Output = 5.0; else if (S == 6.0) Output = 6.0; else Output = 0.0; //@assert(range check)[!(Output <= 6 && Output >= 0)] return Output; }

which CBMC translates to:

`; SMT 2 (set-info :source "Generated by CBMC 5.4") (set-option :produce-models true) (set-logic QF_AUFBV)

; convert (define-fun |B1| () Bool |goto_symex::&92;guard#1|)

; convert (define-fun |B2| () Bool (not |goto_symex::&92;guard#1|))

; convert (define-fun |B4| () Bool (and (not |goto_symex::&92;guard#1|) |goto_symex::&92;guard#2|))

; convert (define-fun |B5| () Bool (and (not |goto_symex::&92;guard#1|) (not |goto_symex::&92;guard#2|)))

; convert (define-fun |B7| () Bool (and (not |goto_symex::&92;guard#1|) (not |goto_symex::&92;guard#2|) |goto_symex::&92;guard#3|))

; convert (define-fun |B8| () Bool (and (not |goto_symex::&92;guard#1|) (not |goto_symex::&92;guard#2|) (not |goto_symex::&92;guard#3|)))

; convert (define-fun |B10| () Bool (and (not |goto_symex::&92;guard#1|) (not |goto_symex::&92;guard#2|) (not |goto_symex::&92;guard#3|) |goto_symex::&92;guard#4|))

; convert (define-fun |B11| () Bool (and (not |goto_symex::&92;guard#1|) (not |goto_symex::&92;guard#2|) (not |goto_symex::&92;guard#3|) (not |goto_symex::&92;guard#4|)))

; convert (define-fun |B13| () Bool (and (not |goto_symex::&92;guard#1|) (not |goto_symex::&92;guard#2|) (not |goto_symex::&92;guard#3|) (not |goto_symex::&92;guard#4|) |goto_symex::&92;guard#5|))

; convert (define-fun |B14| () Bool (and (not |goto_symex::&92;guard#1|) (not |goto_symex::&92;guard#2|) (not |goto_symex::&92;guard#3|) (not |goto_symex::&92;guard#4|) (not |goto_symex::&92;guard#5|)))

; find_symbols (declare-fun |goto_symex::&92;guard#6| () Bool) ; convert (define-fun |B15| () Bool (and (not |goto_symex::&92;guard#1|) (not |goto_symex::&92;guard#2|) (not |goto_symex::&92;guard#3|) (not |goto_symex::&92;guard#4|) (not |goto_symex::&92;guard#5|) |goto_symex::&92;guard#6|))

; convert (define-fun |B16| () Bool (and (not |goto_symex::&92;guard#1|) (not |goto_symex::&92;guard#2|) (not |goto_symex::&92;guard#3|) (not |goto_symex::&92;guard#4|) (not |goto_symex::&92;guard#5|) |goto_symex::&92;guard#6|))

; convert (define-fun |B17| () Bool (and (not |goto_symex::&92;guard#1|) (not |goto_symex::&92;guard#2|) (not |goto_symex::&92;guard#3|) (not |goto_symex::&92;guard#4|) (not |goto_symex::&92;guard#5|) (not |goto_symex::&92;guard#6|)))

; find_symbols (declare-fun |goto_symex::&92;guard#7| () Bool) ; convert (define-fun |B18| () Bool (and (not |goto_symex::&92;guard#1|) (not |goto_symex::&92;guard#2|) (not |goto_symex::&92;guard#3|) (not |goto_symex::&92;guard#4|) (not |goto_symex::&92;guard#5|) (not |goto_symex::&92;guard#6|) |goto_symex::&92;guard#7|))

; convert (define-fun |B19| () Bool (and (not |goto_symex::&92;guard#1|) (not |goto_symex::&92;guard#2|) (not |goto_symex::&92;guard#3|) (not |goto_symex::&92;guard#4|) (not |goto_symex::&92;guard#5|) (not |goto_symex::&92;guard#6|) |goto_symex::&92;guard#7|))

; convert (define-fun |B20| () Bool (and (not |goto_symex::&92;guard#1|) (not |goto_symex::&92;guard#2|) (not |goto_symex::&92;guard#3|) (not |goto_symex::&92;guard#4|) (not |goto_symex::&92;guard#5|) (not |goto_symex::&92;guard#6|) (not |goto_symex::&92;guard#7|)))

; set_to true (equal) (define-fun |__CPROVER_deadobject#1| () ( BitVec 64) (_ bv0 64))

; set_to true (equal) (define-fun |__CPROVERdeallocated#1| () ( BitVec 64) (_ bv0 64))

; set_to true (equal) (define-fun |__CPROVER_malloc_is_new_array#1| () Bool false)

; set_to true (equal) (define-fun |__CPROVER_mallocobject#1| () ( BitVec 64) (_ bv0 64))

; set_to true (equal) (define-fun |__CPROVER_mallocsize#1| () ( BitVec 64) (_ bv0 64))

; set_to true (equal) (define-fun |__CPROVER_memoryleak#1| () ( BitVec 64) (_ bv0 64))

; set_to true (equal) (define-fun |__CPROVER_next_threadid#1| () ( BitVec 64) (_ bv0 64))

; set_to true (equal) (define-fun |__CPROVER_pipecount#1| () ( BitVec 32) (_ bv0 32))

; set_to true (equal) (define-fun |__CPROVER_roundingmode!0#1| () ( BitVec 32) (_ bv0 32))

; set_to true (equal) (define-fun |__CPROVER_threadid!0#1| () ( BitVec 64) (_ bv0 64))

; the following is a substitute for lambda i. x (declare-fun arrayof.0 () (Array ( BitVec 64) (_ BitVec 1))) ; set_to true (equal) (define-fun |__CPROVER_threadsexited#1| () (Array ( BitVec 64) (_ BitVec 1)) array_of.0)

; find_symbols (declare-fun |main::1::HIS!0@1#1| () ( BitVec 32)) ; this is a model for floatbv_typecast : f32_23 -> f64_52 (define-fun |float_bv.floatbv_typecast_f32_23->f6452| ((op0 ( BitVec 32)) (op1 ( BitVec 32))) ( BitVec 64) (let ((|_let1| (( extract 30 23) op0))) (let ((|_let_2| (= |_let1| ( bv255 8)))) (let ((|_let3| (( extract 22 0) op0))) (let ((|_let_4| (= |_let3| ( bv0 23)))) (let ((|_let_6| (and |_let_2| (not |_let_4|)))) (let ((|_let_9| (and |_let_2| |_let_4|))) (let ((|_let_11| (= |_let1| ( bv0 8)))) (let ((|_let_16| (concat (concat (ite (and (not |_let_11|) (not |_let_2|)) #b1 #b0) |_let3|) ( bv0 29)))) (let ((|_let18| (= (( extract 52 21) |_let16|) ( bv0 32)))) (let ((|_let_20| (ite |_let_18| (bvshl |_let16| ( bv32 53)) |_let_16|))) (let ((|_let22| (= (( extract 52 37) |_let20|) ( bv0 16)))) (let ((|_let_24| (ite |_let_22| (bvshl |_let20| ( bv16 53)) |_let_20|))) (let ((|_let26| (= (( extract 52 45) |_let24|) ( bv0 8)))) (let ((|_let_28| (ite |_let_26| (bvshl |_let24| ( bv8 53)) |_let_24|))) (let ((|_let30| (= (( extract 52 49) |_let28|) ( bv0 4)))) (let ((|_let_32| (ite |_let_30| (bvshl |_let28| ( bv4 53)) |_let_28|))) (let ((|_let34| (= (( extract 52 51) |_let32|) ( bv0 2)))) (let ((|_let_36| (ite |_let_34| (bvshl |_let32| ( bv2 53)) |_let_32|))) (let ((|_let38| (= (( extract 52 52) |_let36|) ( bv0 1)))) (let ((|_let_40| (ite |_let_38| (bvshl |_let36| ( bv1 53)) |_let_36|))) (concat (ite (ite |_let6| false (= (( extract 31 31) op0) #b1)) #b1 #b0) (concat (ite (or |_let_6| |_let9|) ( bv2047 11) (ite (not (= ((_ extract 52 52) |_let40|) #b1)) ( bv0 11) (bvadd (bvsub ((_ sign_extend 3) (ite |_let11| ( bv130 8) (bvsub |_let1| ( bv127 8)))) (bvor (bvor (bvor (bvor (bvor (bvor (_ bv0 11) (bvshl (ite |_let18| ( bv1 11) ( bv0 11)) ( bv5 11))) (bvshl (ite |_let22| ( bv1 11) ( bv0 11)) ( bv4 11))) (bvshl (ite |_let26| ( bv1 11) ( bv0 11)) ( bv3 11))) (bvshl (ite |_let30| ( bv1 11) ( bv0 11)) ( bv2 11))) (bvshl (ite |_let34| ( bv1 11) ( bv0 11)) ( bv1 11))) (bvshl (ite |_let38| ( bv1 11) ( bv0 11)) ( bv0 11)))) (_ bv1023 11)))) (ite |_let6| ( bv1 52) (ite |_let9| ( bv0 52) ((_ extract 51 0) |_let_40|)))))))))))))))))))))))))) ; this is a model for ieee_float_equal : f64_52 -> b (define-fun |float_bv.ieee_float_equal_f6452->b| ((op0 ( BitVec 64)) (op1 ( BitVec 64))) Bool (and (or (= op0 op1) (and (= (bvand op0 ( bv9223372036854775807 64)) ( bv0 64)) (= (bvand op1 ( bv9223372036854775807 64)) ( bv0 64)))) (not (or (and (= (( extract 62 52) op0) ( bv2047 11)) (not (= (( extract 51 0) op0) ( bv0 52)))) (and (= (( extract 62 52) op1) ( bv2047 11)) (not (= (( extract 51 0) op1) (_ bv0 52)))))))) ; set_to true (assert (= |goto_symex::&92;guard#1| (|float_bv.ieee_float_equal_f64_52->b| (|float_bv.floatbv_typecast_f32_23->f64_52| |main::1::HIS!0@1#1| ( bv0 32)) (_ bv0 64))))

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#2| () ( BitVec 32) (_ bv0 32))

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#4| () ( BitVec 32) (_ bv1065353216 32))

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#5| () ( BitVec 32) |main::1::LO_Output!0@1#3|)

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#6| () ( BitVec 32) (_ bv1073741824 32))

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#7| () ( BitVec 32) |main::1::LO_Output!0@1#5|)

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#8| () ( BitVec 32) (_ bv1077936128 32))

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#9| () ( BitVec 32) |main::1::LO_Output!0@1#7|)

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#10| () ( BitVec 32) (_ bv1082130432 32))

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#11| () ( BitVec 32) |main::1::LO_Output!0@1#9|)

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#12| () ( BitVec 32) (_ bv1084227584 32))

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#13| () ( BitVec 32) |main::1::LO_Output!0@1#11|)

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#14| () ( BitVec 32) (_ bv1086324736 32))

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#15| () ( BitVec 32) |main::1::LO_Output!0@1#13|)

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#16| () ( BitVec 32) (_ bv0 32))

; set_to true (equal) (define-fun |main::1::LOOutput!0@1#17| () ( BitVec 32) (ite |gotosymex::&92;guard#7| ( bv1086324736 32) (_ bv0 32)))

; this is a model for <= : f32_23 -> b (define-fun |float_bv.<=_f3223->b| ((op0 ( BitVec 32)) (op1 (_ BitVec 32))) Bool (let ((|_let97| (= (( extract 31 31) op0) #b1))) (let ((|_let98| (= (( extract 31 31) op1) #b1))) (and (or (ite (not (= |_let_97| |_let_98|)) |_let_97| (not (= (bvult op0 op1) (and |_let_97| |_let98|)))) (and (= (bvand op0 ( bv2147483647 32)) ( bv0 32)) (= (bvand op1 ( bv2147483647 32)) ( bv0 32))) (= op0 op1)) (not (or (and (= (( extract 30 23) op0) ( bv255 8)) (not (= (( extract 22 0) op0) ( bv0 23)))) (and (= (( extract 30 23) op1) ( bv255 8)) (not (= (( extract 22 0) op1) (_ bv0 23)))))))))) ; set_to true (assert (|float_bv.<=_f32_23->b| |main::1::LOOutput!0@1#23| ( bv1086324736 32)))

; this is a model for >= : f32_23 -> b (define-fun |float_bv.>=_f3223->b| ((op0 ( BitVec 32)) (op1 (_ BitVec 32))) Bool (let ((|_let130| (= (( extract 31 31) op1) #b1))) (let ((|_let131| (= (( extract 31 31) op0) #b1))) (and (or (ite (not (= |_let_130| |_let_131|)) |_let_130| (not (= (bvult op1 op0) (and |_let_130| |_let131|)))) (and (= (bvand op1 ( bv2147483647 32)) ( bv0 32)) (= (bvand op0 ( bv2147483647 32)) ( bv0 32))) (= op1 op0)) (not (or (and (= (( extract 30 23) op1) ( bv255 8)) (not (= (( extract 22 0) op1) ( bv0 23)))) (and (= (( extract 30 23) op0) ( bv255 8)) (not (= (( extract 22 0) op0) (_ bv0 23)))))))))) ; set_to true (assert (|float_bv.>=_f32_23->b| |main::1::LOOutput!0@1#23| ( bv0 32)))

(check-sat) (exit) ; end of SMT2 file `

taking |main::1::HI_S!0@1#1| as non-deterministic input and |main::1::LO_Output!0@1#23| as random output which depends on the input, z3 parses that smtlib2 string to this expression:

`(let ((a!1 (and (= ((_ extract 30 23) |main::1::HIS!0@1#1|) #xff) (not (= (( extract 22 0) |main::1::HI_S!0@1#1|)

b00000000000000000000000))))

  (a!4 (and (not (= ((_ extract 30 23) |main::1::HI_S!0@1#1|) #x00))
            (not (= ((_ extract 30 23) |main::1::HI_S!0@1#1|) #xff))))
  (a!15 ((_ sign_extend 3)
          (ite (= ((_ extract 30 23) |main::1::HI_S!0@1#1|) #x00)
               #x82
               (bvsub ((_ extract 30 23) |main::1::HI_S!0@1#1|) #x7f))))
  (a!28 (and (= ((_ extract 62 52) #x0000000000000000) #b11111111111)
             (not (= ((_ extract 51 0) #x0000000000000000) #x0000000000000))))
  (a!32 (and (= ((_ extract 62 52) #x3ff0000000000000) #b11111111111)
             (not (= ((_ extract 51 0) #x3ff0000000000000) #x0000000000000))))
  (a!36 (and (= ((_ extract 62 52) #x4000000000000000) #b11111111111)
             (not (= ((_ extract 51 0) #x4000000000000000) #x0000000000000))))
  (a!40 (and (= ((_ extract 62 52) #x4008000000000000) #b11111111111)
             (not (= ((_ extract 51 0) #x4008000000000000) #x0000000000000))))
  (a!44 (and (= ((_ extract 62 52) #x4010000000000000) #b11111111111)
             (not (= ((_ extract 51 0) #x4010000000000000) #x0000000000000))))
  (a!48 (and (= ((_ extract 62 52) #x4014000000000000) #b11111111111)
             (not (= ((_ extract 51 0) #x4014000000000000) #x0000000000000))))
  (a!52 (and (= ((_ extract 62 52) #x4018000000000000) #b11111111111)
             (not (= ((_ extract 51 0) #x4018000000000000) #x0000000000000))))
  (a!54 (ite |goto_symex::&92;guard#4|
             #x40400000
             (ite |goto_symex::&92;guard#5|
                  #x40800000
                  (ite |goto_symex::&92;guard#6|
                       #x40a00000
                       (ite |goto_symex::&92;guard#7| #x40c00000 #x00000000)))))
  (a!60 (and (= ((_ extract 30 23) #x40c00000) #xff)
             (not (= ((_ extract 22 0) #x40c00000)
                     #b00000000000000000000000))))
  (a!64 (and (= ((_ extract 30 23) #x00000000) #xff)
             (not (= ((_ extract 22 0) #x00000000)
                     #b00000000000000000000000)))))

(let ((a!2 (ite (ite a!1 false (= ((_ extract 31 31) |main::1::HI_S!0@1#1|) #b1))

b1

            #b0))
  (a!3 (or a!1
           (and (= ((_ extract 30 23) |main::1::HI_S!0@1#1|) #xff)
                (= ((_ extract 22 0) |main::1::HI_S!0@1#1|)
                   #b00000000000000000000000))))
  (a!5 ((_ extract 52 21)
         (concat (concat (ite a!4 #b1 #b0)
                         ((_ extract 22 0) |main::1::HI_S!0@1#1|))
                 #b00000000000000000000000000000)))
  (a!6 (bvshl (concat (concat (ite a!4 #b1 #b0)
                              ((_ extract 22 0) |main::1::HI_S!0@1#1|))
                      #b00000000000000000000000000000)
              #b00000000000000000000000000000000000000000000000100000))
  (a!55 (ite |goto_symex::&92;guard#1|
             #x00000000
             (ite |goto_symex::&92;guard#2|
                  #x3f800000
                  (ite |goto_symex::&92;guard#3| #x40000000 a!54)))))

(let ((a!7 (ite (= a!5 #x00000000) a!6 (concat (concat (ite a!4 #b1 #b0) ((_ extract 22 0) |main::1::HI_S!0@1#1|))

b00000000000000000000000000000)))

  (a!56 (not (= (= ((_ extract 31 31) a!55) #b1)
                (= ((_ extract 31 31) #x40c00000) #b1))))
  (a!57 (= (bvult a!55 #x40c00000)
           (and (= ((_ extract 31 31) a!55) #b1)
                (= ((_ extract 31 31) #x40c00000) #b1))))
  (a!59 (and (= ((_ extract 30 23) a!55) #xff)
             (not (= ((_ extract 22 0) a!55) #b00000000000000000000000))))
  (a!61 (not (= (= ((_ extract 31 31) #x00000000) #b1)
                (= ((_ extract 31 31) a!55) #b1))))
  (a!62 (= (bvult #x00000000 a!55)
           (and (= ((_ extract 31 31) #x00000000) #b1)
                (= ((_ extract 31 31) a!55) #b1)))))

(let ((a!8 (( extract 52 45) (ite (= (( extract 52 37) a!7) #x0000) (bvshl a!7

b00000000000000000000000000000000000000000000000010000)

              a!7)))
  (a!9 (bvshl (ite (= ((_ extract 52 37) a!7) #x0000)
                   (bvshl a!7
                          #b00000000000000000000000000000000000000000000000010000)
                   a!7)
              #b00000000000000000000000000000000000000000000000001000))
  (a!16 (bvshl (ite (= ((_ extract 52 37) a!7) #x0000)
                    #b00000000001
                    #b00000000000)
               #b00000000100))
  (a!58 (or (ite a!56 (= ((_ extract 31 31) a!55) #b1) (not a!57))
            (and (= (bvand a!55 #x7fffffff) #x00000000)
                 (= (bvand #x40c00000 #x7fffffff) #x00000000))
            (= a!55 #x40c00000)))
  (a!63 (or (ite a!61 (= ((_ extract 31 31) #x00000000) #b1) (not a!62))
            (and (= (bvand #x00000000 #x7fffffff) #x00000000)
                 (= (bvand a!55 #x7fffffff) #x00000000))
            (= #x00000000 a!55))))

(let ((a!10 (ite (= a!8 #x00) a!9 (ite (= ((_ extract 52 37) a!7) #x0000) (bvshl a!7

b00000000000000000000000000000000000000000000000010000)

                  a!7))))

(let ((a!11 (( extract 52 51) (ite (= (( extract 52 49) a!10) #x0) (bvshl a!10

b00000000000000000000000000000000000000000000000000100)

               a!10)))
  (a!12 (bvshl (ite (= ((_ extract 52 49) a!10) #x0)
                    (bvshl a!10
                           #b00000000000000000000000000000000000000000000000000100)
                    a!10)
               #b00000000000000000000000000000000000000000000000000010))
  (a!17 (bvshl (ite (= ((_ extract 52 49) a!10) #x0)
                    #b00000000001
                    #b00000000000)
               #b00000000010)))

(let ((a!13 (ite (= a!11 #b00) a!12 (ite (= ((_ extract 52 49) a!10) #x0) (bvshl a!10

b00000000000000000000000000000000000000000000000000100)

                  a!10))))

(let ((a!14 (( extract 52 52) (ite (= (( extract 52 52) a!13) #b0) (bvshl a!13

b00000000000000000000000000000000000000000000000000001)

               a!13)))
  (a!18 (bvshl (ite (= ((_ extract 52 52) a!13) #b0)
                    #b00000000001
                    #b00000000000)
               #b00000000000))
  (a!21 ((_ extract 51 0)
          (ite (= ((_ extract 52 52) a!13) #b0)
               (bvshl a!13
                      #b00000000000000000000000000000000000000000000000000001)
               a!13))))

(let ((a!19 (bvor #b00000000000 (bvshl (ite (= a!5 #x00000000) #b00000000001 #b00000000000)

b00000000101)

              a!16
              (bvshl (ite (= a!8 #x00) #b00000000001 #b00000000000)
                     #b00000000011)
              a!17
              (bvshl (ite (= a!11 #b00) #b00000000001 #b00000000000)
                     #b00000000001)
              a!18))
  (a!22 (ite (and (= ((_ extract 30 23) |main::1::HI_S!0@1#1|) #xff)
                  (= ((_ extract 22 0) |main::1::HI_S!0@1#1|)
                     #b00000000000000000000000))
             #x0000000000000
             a!21)))

(let ((a!20 (ite a!3

b11111111111

             (ite (not (= a!14 #b1))
                  #b00000000000
                  (bvadd (bvsub a!15 a!19) #b01111111111)))))

(let ((a!23 (= (concat a!2 (concat a!20 (ite a!1 #x0000000000001 a!22)))

x0000000000000000))

  (a!24 (bvand (concat a!2 (concat a!20 (ite a!1 #x0000000000001 a!22)))
               #x7fffffffffffffff))
  (a!26 ((_ extract 62 52)
          (concat a!2 (concat a!20 (ite a!1 #x0000000000001 a!22)))))
  (a!27 ((_ extract 51 0)
          (concat a!2 (concat a!20 (ite a!1 #x0000000000001 a!22)))))
  (a!30 (= (concat a!2 (concat a!20 (ite a!1 #x0000000000001 a!22)))
           #x3ff0000000000000))
  (a!34 (= (concat a!2 (concat a!20 (ite a!1 #x0000000000001 a!22)))
           #x4000000000000000))
  (a!38 (= (concat a!2 (concat a!20 (ite a!1 #x0000000000001 a!22)))
           #x4008000000000000))
  (a!42 (= (concat a!2 (concat a!20 (ite a!1 #x0000000000001 a!22)))
           #x4010000000000000))
  (a!46 (= (concat a!2 (concat a!20 (ite a!1 #x0000000000001 a!22)))
           #x4014000000000000))
  (a!50 (= (concat a!2 (concat a!20 (ite a!1 #x0000000000001 a!22)))
           #x4018000000000000)))

(let ((a!25 (or a!23 (and (= a!24 #x0000000000000000) (= (bvand #x0000000000000000 #x7fffffffffffffff)

x0000000000000000))))

  (a!29 (or (and (= a!26 #b11111111111) (not (= a!27 #x0000000000000)))
            a!28))
  (a!31 (or a!30
            (and (= a!24 #x0000000000000000)
                 (= (bvand #x3ff0000000000000 #x7fffffffffffffff)
                    #x0000000000000000))))
  (a!33 (or (and (= a!26 #b11111111111) (not (= a!27 #x0000000000000)))
            a!32))
  (a!35 (or a!34
            (and (= a!24 #x0000000000000000)
                 (= (bvand #x4000000000000000 #x7fffffffffffffff)
                    #x0000000000000000))))
  (a!37 (or (and (= a!26 #b11111111111) (not (= a!27 #x0000000000000)))
            a!36))
  (a!39 (or a!38
            (and (= a!24 #x0000000000000000)
                 (= (bvand #x4008000000000000 #x7fffffffffffffff)
                    #x0000000000000000))))
  (a!41 (or (and (= a!26 #b11111111111) (not (= a!27 #x0000000000000)))
            a!40))
  (a!43 (or a!42
            (and (= a!24 #x0000000000000000)
                 (= (bvand #x4010000000000000 #x7fffffffffffffff)
                    #x0000000000000000))))
  (a!45 (or (and (= a!26 #b11111111111) (not (= a!27 #x0000000000000)))
            a!44))
  (a!47 (or a!46
            (and (= a!24 #x0000000000000000)
                 (= (bvand #x4014000000000000 #x7fffffffffffffff)
                    #x0000000000000000))))
  (a!49 (or (and (= a!26 #b11111111111) (not (= a!27 #x0000000000000)))
            a!48))
  (a!51 (or a!50
            (and (= a!24 #x0000000000000000)
                 (= (bvand #x4018000000000000 #x7fffffffffffffff)
                    #x0000000000000000))))
  (a!53 (or (and (= a!26 #b11111111111) (not (= a!27 #x0000000000000)))
            a!52)))

which obviously has simplified the random output to some bit vector literals obtained from ite structures' bounds from smtlib2 string. I want to match application expressions and extract predicates which contain random outputs and form a closure of variables in those predicates and mark those which involve some of my non-deterministic inputs. Am i doing it wrong? Or is this just the way it should be?

NikolajBjorner commented 8 years ago

A small example would be easier to understand, but I believe I see what the issue is: You define output bits using (define-fun ...) construct and inputs are (declare-fun ..). (declare-fun ...) lets you create free variables while (define-fun ..) lets you create macros. The macros are expanded inside the parser. If you want to retain the macros as equalities, then you will have to use (declare-fun ...) followed by assertion of an equality.

      ; set_to true (equal)
      (define-fun |main::1::LO_Output!0@1#10| () (_ BitVec 32) (_ bv1082130432 32))

becomes

   (declare-fun |main::1::LO_Output!0@1#10| () (_ BitVec 32))
   (assert (= |main::1::LO_Output!0@1#10| (_ bv1082130432 32)))

To recover the output variables you would then have to walk the resulting formula.

kooshan commented 8 years ago

Thank you for your amazingly fast response. This indeed solved my problem.

Z3Prover / z3

Z3_parse_smtlib2_string function simplifies and rules out some variables to literals #635

b00000000000000000000000))))

b1

b00000000000000000000000000000)))

b00000000000000000000000000000000000000000000000010000)

b00000000000000000000000000000000000000000000000010000)

b00000000000000000000000000000000000000000000000000100)

b00000000000000000000000000000000000000000000000000100)

b00000000000000000000000000000000000000000000000000001)

b00000000101)

b11111111111

x0000000000000000))

x0000000000000000))))