[agusaldasoro]

Problem

BLOB columns had no entry in TYPE_MAP. Every table of the schema is declared for every query, so a single BLOB column made SMT-LIB generation fail for all queries of the schema.

The value also needs care. H2 1.4 reads a string literal given for a binary column as hexadecimal, so a value such as "abc" makes it reject the INSERT (Hexadecimal string with odd number of characters). H2 2.x, MySQL and PostgreSQL accept any text.

Fix

• SmtLibGenerator.BLOB_TYPES: maps every spelling to String:
  • BINARY LARGE OBJECT (H2 2.x)
  • BLOB (H2 1.4, MySQL)
  • TINYBLOB, MEDIUMBLOB, LONGBLOB (MySQL)
• SMTLibZ3DbConstraintSolver.binaryValue: on H2, writes the value of a BLOB column as the hex of its UTF-8 bytes, which both H2 versions accept. The mapping is injective, so the equalities the formula imposes (unique and primary keys) still hold. Other databases get the value as is. It is reached from validTextValue (Generate valid UUID, JSON and JSONB values #1849), which handles UUID and JSON columns and passes every other value on.

The values stay plain SMT Strings, so solving costs the same as before.

Tests

• New BlobColumnSolvingTest (H2, Z3 Docker). On master both cases fail, because the solver returns no action:
  • a query on a table with a BLOB column is solved, and the row is inserted and returned by the query;
  • with the column reported as BLOB (as H2 1.4 does), WHERE data = 'abc' produces the value 616263, and the row is inserted.
• UntranslatableQueryCacheTest and UnmappedColumnTypeTest: used a BLOB column as their example of an unmapped type. They now use INTERVAL YEAR.

All tests under org.evomaster.core.database.sql.solver pass.

🤖 Generated with Claude Code

[arcuri82]

@agusaldasoro hi there are merge conflicts

[agusaldasoro]

@agusaldasoro hi there are merge conflicts

Fixed!