CVC4 1.1 released

We are delighted to announce version 1.1 of CVC4, the open-source flagship SMT solver developed at New York University and the University of Iowa, available at

Version 1.1 includes numerous important bug fixes, performance improvements, and usability improvements over the previous stable release (version 1.0).  Additionally, 1.1 features:

  • a new, specialized decision procedure for unsigned bit-vector inequalities
  • improved support for Mac and Windows, and binary releases for these platforms
  • better support for finite model finding, used in conjunction with incremental mode
  • an improved E-matching procedure
  • extended support for Boolean terms in datatypes
  • support for multiline input in interactive mode

We welcome feedback, feature requests, contributions, and collaborations.  It is our hope that CVC4 will become a research platform for a broad and diverse set of users and developers.  If you are interested in getting involved with the project, please contact a member of the development team:

  •   Clark Barrett (NYU, project leader)
  •   Cesare Tinelli (U Iowa, project leader)
  •   Kshitij Bansal (NYU)
  •   François Bobot (Paris-Diderot University)
  •   Chris Conway (Google)
  •   Morgan Deters (NYU)
  •   Liana Hadarean (NYU)
  •   Dejan Jovanović (NYU)
  •   Tim King (NYU)
  •   Tianyi Liang (U Iowa)
  •   Andrew Reynolds (U Iowa)

The development of CVC4 is supported in part by the following organizations:

  • The Air Force Office of Scientific Research (award FA9550-09-1-0596)
  • Intel Corporation
  • The National Science Foundation (grants 0644299,  0914956, 1049495, 1228765, 1228768)
  • The Semiconductor Research Corporation (tasks 1850.001, 1850.002)

Downloads, documentation, tutorials, and more information are available at the CVC4 web site:

-The CVC4 team