Unexpected command error

[recoules]

Hi,

I got an error when I try to solve this formula with boolector: after the big all inclusive assert, any command issue an unexpected command error. Note that this formula is auto-generated (yet it is pretty uggly) but I am confident that it is well formed. The online Z3 demonstrator (https://compsys-tools.ens-lyon.fr/z3/index.php) successfully parses and solves the formula.

Do you have any insight of the problem?

(declare-const !7 (_ BitVec 8))
(declare-const !a (_ BitVec 8))
(declare-const !1 (_ BitVec 32))
(declare-const !y (_ BitVec 32))
(declare-const !b (_ BitVec 8))
(declare-const !9 (_ BitVec 8))
(declare-const !5 (_ BitVec 8))
(declare-const !4 (_ BitVec 8))
(declare-const !3 (_ BitVec 8))
(declare-const !2 (_ BitVec 8))
(declare-const !6 (_ BitVec 8))
(declare-const !8 (_ BitVec 8))
(declare-const !0 (Array (_ BitVec 32) (_ BitVec 8)))
(declare-const !B (_ BitVec 32))
(declare-const !F (_ BitVec 32))
(declare-const !H (_ BitVec 32))
(declare-const !K (_ BitVec 32))
(declare-const !N (_ BitVec 32))
(declare-const !O (_ BitVec 32))
(declare-const !R (_ BitVec 32))
(declare-const !U (_ BitVec 32))
(declare-const !X (_ BitVec 32))
(declare-const !Z (_ BitVec 32))
(declare-const !$ (_ BitVec 32))
(declare-const !& (_ BitVec 32))
(declare-const !- (_ BitVec 32))
(declare-const !/ (_ BitVec 32))
(declare-const != (_ BitVec 32))
(declare-const !? (_ BitVec 32))
(declare-const !^ (_ BitVec 32))
(declare-const $0 (_ BitVec 32))
(declare-const $1 (_ BitVec 32))
(declare-const $2 (_ BitVec 32))
(declare-const $3 (_ BitVec 32))
(declare-const $4 (_ BitVec 32))
(declare-const $6 (_ BitVec 32))
(declare-const $8 (_ BitVec 32))
(declare-const $9 (_ BitVec 32))
(declare-const $a (_ BitVec 32))
(declare-const $b (_ BitVec 32))
(declare-const $c (_ BitVec 32))
(declare-const $d (_ BitVec 32))
(declare-const $f (_ BitVec 32))
(declare-const $h (_ BitVec 32))
(declare-const $j (_ BitVec 32))
(declare-const $n (_ BitVec 32))
(assert (let ((!z #xffffefce)) (let ((!_ #xffffef6c)) (let ((!~ #x0804891e)) (let ((!@ #xffffef70)) (let ((!> #xffffef74)) (let ((!C #x0000001e)) (let ((!< #xffffef78)) (let ((!A #x080da49c)) (let ((!D (concat (select !0 (bvadd !A #x00000003)) (select !0 (bvadd !A #x00000002)) (select !0 (bvadd !A #x00000001)) (select !0 !A)))) (let ((!. #xffffef98)) (let ((!I #xffffeff8)) (let ((!* #xffffef9c)) (let ((!+ #x08048b38)) (let ((!% #xffffefa0)) (let ((!! #xffffefa4)) (let ((!Y #xffffefa8)) (let ((!V #xffffefec)) (let ((!E #x00000014)) (let ((!W (concat (select !0 (bvadd !E #x00000003)) (select !0 (bvadd !E #x00000002)) (select !0 (bvadd !E #x00000001)) (select !0 !E)))) (let ((!S #xffffefbc)) (let ((!G #xfffff008)) (let ((!T (concat (select !0 (bvadd !G #x00000003)) (select !0 (bvadd !G #x00000002)) (select !0 (bvadd !G #x00000001)) (select !0 !G)))) (let ((!P #xffffeff4)) (let ((!Q #xfffff004)) (let ((!L #xffffeffc)) (let ((!J #xfffff000)) (let ((!M (concat (select !0 (bvadd !J #x00000003)) (select !0 (bvadd !J #x00000002)) (select !0 (bvadd !J #x00000001)) (select !0 !J)))) (let (($5 (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store !0 !L ((_ extract 7 0) !M)) (bvadd !L #x00000001) ((_ extract 15 8) !M)) (bvadd !L #x00000002) ((_ extract 23 16) !M)) (bvadd !L #x00000003) ((_ extract 31 24) !M)) !I ((_ extract 7 0) !1)) (bvadd !I #x00000001) ((_ extract 15 8) !1)) (bvadd !I #x00000002) ((_ extract 23 16) !1)) (bvadd !I #x00000003) ((_ extract 31 24) !1)) !P ((_ extract 7 0) !Q)) (bvadd !P #x00000001) ((_ extract 15 8) !Q)) (bvadd !P #x00000002) ((_ extract 23 16) !Q)) (bvadd !P #x00000003) ((_ extract 31 24) !Q)) !S ((_ extract 7 0) !T)) (bvadd !S #x00000001) ((_ extract 15 8) !T)) (bvadd !S #x00000002) ((_ extract 23 16) !T)) (bvadd !S #x00000003) ((_ extract 31 24) !T)) !V ((_ extract 7 0) !W)) (bvadd !V #x00000001) ((_ extract 15 8) !W)) (bvadd !V #x00000002) ((_ extract 23 16) !W)) (bvadd !V #x00000003) ((_ extract 31 24) !W)) !Y ((_ extract 7 0) !D)) (bvadd !Y #x00000001) ((_ extract 15 8) !D)) (bvadd !Y #x00000002) ((_ extract 23 16) !D)) (bvadd !Y #x00000003) ((_ extract 31 24) !D)) !! ((_ extract 7 0) !C)) (bvadd !! #x00000001) ((_ extract 15 8) !C)) (bvadd !! #x00000002) ((_ extract 23 16) !C)) (bvadd !! #x00000003) ((_ extract 31 24) !C)) !% ((_ extract 7 0) !z)) (bvadd !% #x00000001) ((_ extract 15 8) !z)) (bvadd !% #x00000002) ((_ extract 23 16) !z)) (bvadd !% #x00000003) ((_ extract 31 24) !z)) !* ((_ extract 7 0) !+)) (bvadd !* #x00000001) ((_ extract 15 8) !+)) (bvadd !* #x00000002) ((_ extract 23 16) !+)) (bvadd !* #x00000003) ((_ extract 31 24) !+)) !. ((_ extract 7 0) !I)) (bvadd !. #x00000001) ((_ extract 15 8) !I)) (bvadd !. #x00000002) ((_ extract 23 16) !I)) (bvadd !. #x00000003) ((_ extract 31 24) !I)) !< ((_ extract 7 0) !D)) (bvadd !< #x00000001) ((_ extract 15 8) !D)) (bvadd !< #x00000002) ((_ extract 23 16) !D)) (bvadd !< #x00000003) ((_ extract 31 24) !D)) !> ((_ extract 7 0) !C)) (bvadd !> #x00000001) ((_ extract 15 8) !C)) (bvadd !> #x00000002) ((_ extract 23 16) !C)) (bvadd !> #x00000003) ((_ extract 31 24) !C)) !@ ((_ extract 7 0) !z)) (bvadd !@ #x00000001) ((_ extract 15 8) !z)) (bvadd !@ #x00000002) ((_ extract 23 16) !z)) (bvadd !@ #x00000003) ((_ extract 31 24) !z)) !_ ((_ extract 7 0) !~)) (bvadd !_ #x00000001) ((_ extract 15 8) !~)) (bvadd !_ #x00000002) ((_ extract 23 16) !~)) (bvadd !_ #x00000003) ((_ extract 31 24) !~)) !z !2) #xffffefcf !3) #xffffefd0 !4) #xffffefd1 !5))) (let (($7 (concat (select $5 (bvadd !z #x00000003)) (select $5 (bvadd !z #x00000002)) (select $5 (bvadd !z #x00000001)) (select $5 !z)))) (let (($e (store (store (store (store (store (store $5 #xffffefd2 !6) #xffffefd3 !7) #xffffefd4 !8) #xffffefd5 !9) #xffffefd6 !a) #xffffefd7 !b))) (let (($g #x0000000c)) (let (($k #x00000000)) (let (($i #x080dbef8)) (let (($l (concat (select !0 (bvadd $i #x00000003)) (select !0 (bvadd $i #x00000002)) (select !0 (bvadd $i #x00000001)) (select !0 $i)))) (let (($m #x00000010)) (and (not (= $7 #x31444d43)) (not (= $7 #x32444d43)) (= (concat (select $e (bvadd !z #x00000009)) (select $e (bvadd !z #x00000008)) (select $e (bvadd !z #x00000007)) (select $e (bvadd !z #x00000006)) (select $e (bvadd !z #x00000005)) (select $e (bvadd !z #x00000004)) (select $e (bvadd !z #x00000003)) (select $e (bvadd !z #x00000002)) (select $e (bvadd !z #x00000001)) (select $e !z)) (_ bv322546174813794243725640 80)) (not (= (concat (select !0 (bvadd $g #x00000003)) (select !0 (bvadd $g #x00000002)) (select !0 (bvadd $g #x00000001)) (select !0 $g)) $k)) (not (= $l $k)) (not (= (bvsub $k $l) $k)) (= (bvsub $l #x00000002) $k) (= !y (concat (select !0 (bvadd $m #x00000003)) (select !0 (bvadd $m #x00000002)) (select !0 (bvadd $m #x00000001)) (select !0 $m))) (= !B !A) (= !F !E) (= !H !G) (= !K !J) (= !N !L) (= !O !I) (= !R !P) (= !U !S) (= !X !V) (= !Z !Y) (= !$ !!) (= !& !%) (= !- !*) (= !/ !.) (= != !<) (= !? !>) (= !^ !@) (= $0 !_) (= $1 !z) (= $2 #xffffefcf) (= $3 #xffffefd0) (= $4 #xffffefd1) (= $6 !z) (= $8 #xffffefd2) (= $9 #xffffefd3) (= $a #xffffefd4) (= $b #xffffefd5) (= $c #xffffefd6) (= $d #xffffefd7) (= $f !z) (= $h $g) (= $j $i) (= $n $m))))))))))))))))))))))))))))))))))))))
(check-sat)

[aytey]

What version of Boolector are using? I just tried with 4d24043 and got sat on your file; I then added some assertions/declarations after your assert and I also got what I would expect:

sat
(
  (define-fun !7 () (_ BitVec 8) #b01001110)
  (define-fun !a () (_ BitVec 8) #b01001101)
  (define-fun !1 () (_ BitVec 32) #b00000000000000000000000000000000)
  (define-fun !y () (_ BitVec 32) #b00000000000000000000000000000000)
  (define-fun !b () (_ BitVec 8) #b01000100)
  (define-fun !9 () (_ BitVec 8) #b01000011)
  (define-fun !5 () (_ BitVec 8) #b01000100)
  (define-fun !4 () (_ BitVec 8) #b01000100)
  (define-fun !3 () (_ BitVec 8) #b01001001)
  (define-fun !2 () (_ BitVec 8) #b01001000)
  (define-fun !6 () (_ BitVec 8) #b01000101)
  (define-fun !8 () (_ BitVec 8) #b01011111)
  (define-fun !0 (
   (!0_x0 (_ BitVec 32))) (_ BitVec 8)
    (ite (= !0_x0 #b00001000000011011011111011111000) #b00000010
    (ite (= !0_x0 #b00000000000000000000000000001111) #b00000001
    (ite (= !0_x0 #b00000000000000000000000000001110) #b00000001
    (ite (= !0_x0 #b00000000000000000000000000001101) #b00000001
    (ite (= !0_x0 #b00000000000000000000000000001100) #b00000001
    (ite (= !0_x0 #b00000000000000000000000000010011) #b00000000
    (ite (= !0_x0 #b00000000000000000000000000010010) #b00000000
    (ite (= !0_x0 #b00000000000000000000000000010001) #b00000000
    (ite (= !0_x0 #b00000000000000000000000000010000) #b00000000
    (ite (= !0_x0 #b00001000000011011011111011111001) #b00000000
    (ite (= !0_x0 #b00001000000011011011111011111010) #b00000000
    (ite (= !0_x0 #b00001000000011011011111011111011) #b00000000
      #b00000000)))))))))))))
  (define-fun !B () (_ BitVec 32) #b00001000000011011010010010011100)
  (define-fun !F () (_ BitVec 32) #b00000000000000000000000000010100)
  (define-fun !H () (_ BitVec 32) #b11111111111111111111000000001000)
  (define-fun !K () (_ BitVec 32) #b11111111111111111111000000000000)
  (define-fun !N () (_ BitVec 32) #b11111111111111111110111111111100)
  (define-fun !O () (_ BitVec 32) #b11111111111111111110111111111000)
  (define-fun !R () (_ BitVec 32) #b11111111111111111110111111110100)
  (define-fun !U () (_ BitVec 32) #b11111111111111111110111110111100)
  (define-fun !X () (_ BitVec 32) #b11111111111111111110111111101100)
  (define-fun !Z () (_ BitVec 32) #b11111111111111111110111110101000)
  (define-fun !$ () (_ BitVec 32) #b11111111111111111110111110100100)
  (define-fun !& () (_ BitVec 32) #b11111111111111111110111110100000)
  (define-fun !- () (_ BitVec 32) #b11111111111111111110111110011100)
  (define-fun !/ () (_ BitVec 32) #b11111111111111111110111110011000)
  (define-fun != () (_ BitVec 32) #b11111111111111111110111101111000)
  (define-fun !? () (_ BitVec 32) #b11111111111111111110111101110100)
  (define-fun !^ () (_ BitVec 32) #b11111111111111111110111101110000)
  (define-fun $0 () (_ BitVec 32) #b11111111111111111110111101101100)
  (define-fun $1 () (_ BitVec 32) #b11111111111111111110111111001110)
  (define-fun $2 () (_ BitVec 32) #b11111111111111111110111111001111)
  (define-fun $3 () (_ BitVec 32) #b11111111111111111110111111010000)
  (define-fun $4 () (_ BitVec 32) #b11111111111111111110111111010001)
  (define-fun $6 () (_ BitVec 32) #b11111111111111111110111111001110)
  (define-fun $8 () (_ BitVec 32) #b11111111111111111110111111010010)
  (define-fun $9 () (_ BitVec 32) #b11111111111111111110111111010011)
  (define-fun $a () (_ BitVec 32) #b11111111111111111110111111010100)
  (define-fun $b () (_ BitVec 32) #b11111111111111111110111111010101)
  (define-fun $c () (_ BitVec 32) #b11111111111111111110111111010110)
  (define-fun $d () (_ BitVec 32) #b11111111111111111110111111010111)
  (define-fun $f () (_ BitVec 32) #b11111111111111111110111111001110)
  (define-fun $h () (_ BitVec 32) #b00000000000000000000000000001100)
  (define-fun $j () (_ BitVec 32) #b00001000000011011011111011111000)
  (define-fun $n () (_ BitVec 32) #b00000000000000000000000000010000)
  (define-fun abc () (_ BitVec 8) #b00001000)
)

(abc is what I added)

[recoules]

Thank you for your quick answer, I was off by several months (august 2019) but being in sync with master does not solve the problem.

Really strange, I get the error only when I run boolector interactively in stdin. If I feed the formula in a file, it works fine, but if I run

boolector -i -m

I got:

boolector: <stdin>:48:2: unexpected command 'check-sat'

The tool that generated the formula directly feed it in pipe so the problem arise.

[aytey]

I'm on macOS and using iTerm, if I do this:

• copy your SMT2 instance
• cat > moo.smt2
• paste

then I get a truncated file (to get it working, I used vim with :set paste).

I then I had to use this: https://unix.stackexchange.com/a/204820 ; basically:

• copy your SMT2 instance
• stty -icanon; cat > moo.smt2
• paste
• stty sane

which then gave me the full content.

Basically, this probably isn't a Boolector issue, but a terminal/shell issue.

[recoules]

Hum, sorry for this inconvenience, you should be right, it is only a buffer problem. Have a nice day,