Mentions légales du service

Skip to content

Support for dreal prover

MARCHE Claude requested to merge dreal into master

The following have been added to have support for the dReal prover :

  • A new driver
  • A new transformation to eliminate non arithmetic assertions
  • A small correction on the smtv2 printer to avoid printing newlines on commentaries
  • A small change in the ieee_float theory to have constants defined by axioms so that we can remove them in the drivers with the remove prop construct.
Edited by BONNOT Paul

Merge request reports