z3 SMT solver: unknown result after running QF_BVRE benchmark

3
votes

I just downloaded the benchmarks for seq and regexp sorts (using z3-4.3.2). What could be the problem when I get unknown as result after running "membership_1.smt2"?

I did not specify any further command line options. According to the benchmark it should result in sat, but unknown is printed without any model.

Thank you

edit:

I noticed further, that "re-begin" is not recognized. Has this to do with the version of z3 or did u just forgot a command line option?

1
z3smt
You are right, the command "re-begin" is not recognized and the command "re-concat" is not recognized too. – Juan Ospina

1 Answers

0
votes

Firstly, I don't know where the OP or commenter found the "membership_1.smt2" example input. I checked the SMT-LIB benchmarks, and the source of Z3, S3, and Z3-str, and couldn't find it.

In any case, the problem was that the OP was testing a benchmark written either for S3 or Z3-str and running it against an unmodified version of Z3. S3 and Z3-str require a modified version of Z3 to handle these extensions. This is described on the S3 website [S3: A Symbolic String Solver for Web Security Analysis, http://www.comp.nus.edu.sg/~trinhmt/S3/, accessed Aug. 4, 2016]:

Modified Version of Z3 Solver

  • The source code of the modified Z3 is available here.
  • We modify Z3 to have the interaction between String theory and Arithmetic theory.

  • These newly-added API methods allows us to query the length of a string variable, and relationship between the length of different string variables, as shown in our CCS'14 paper.

  • Our modified version of Z3 is also used by Z3-str GROUP for integer/string theory integration.

Grepping the (unmodified) Z3 source shows no matches for "re-begin" or "re-concat". Grepping the modified version shows that these tokes are defined in lib/seq_decl_plugin.cpp of z3-source-060115.zip.