PV4 Z3str3REpart of Z3, produces a satisfiability result for a set of constrains

Application domain/field

Type of tool

Algorithm for SMT solving


Implemented as part of Z3 for solving regex constraints and linear integer arithmetic over length of string terms.


Artifact/reproduction package for CAV '21 paper: https://figshare.com/s/5ae73a6f3c55f5c5e4c1

Related papers

An SMT Solver for Regular Expressions and Linear Arithmetic over String Length (CAV '21)

Last publication date

15 July 2021

Related tools

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.