Z3 parsing error

[redianthus]

Hi @filipeom,

Here is another one from Owi, which seems quite weird to me!

$ owi c testcomp/sv-benchmarks/c/fuzzle-programs/07_fuzzle_50x50_25-cycle.c  -vvv
...
owi: [DEBUG] path condition smt query:
              (let-const symbol_2 i8)
              (let-const symbol_4 i8)
              (let-const symbol_5 i8)
              (let-const symbol_0 i8)
              (assert (i32.le_s (i32 0) (i32.extend_i24_u symbol_0)))
              (assert (i32.lt_s (i32 -44) (i32.extend_i24_u symbol_2)))
              (assert (i32.lt_s (i32 41) (i32.extend_i24_u symbol_2)))
              (assert (i32.lt_s (i32 -44) (i32.extend_i24_u symbol_4)))
              (assert (i32.le_s (i32.extend_i24_u symbol_4) (i32 41)))
              (assert (i32.lt_s (i32 -1) (i32.extend_i24_u symbol_5)))
              (check-sat)
owi: internal error, uncaught exception:
     Z3.Error("parser error")

[filipeom]

Whaat, this is super odd. I've never had a parser error before 😓 Was this in owi main branch?

[redianthus]

It was on main indeed, I can easily reproduce. (I fixed the file name which was wrong)

[hra687261]

In #475 I could not reproduce the error from the query in this issue (Once I fixed the parsing issue and without the fix in #474)

[redianthus]

I'm closing because it was fixed for me too. :)