support for cut generation by theory solvers; in progress
fixing issue with warning 44
Merge branch 'master' of login.ccs.neu.edu:repositories/bct
pretty-print formulas in SMT-LIB format (entirely untested)
completed smtlib_printer; db_solver can now produce SMT-LIB output
forgotten bounds module
updating for current dequeue API
missing modules in OMakefile
SMT-LIB generation fixes (again)
minor fix: no longer calling SCIPtransformVar & co. in creation stage
faster SMT-LIB printing plus usability improvements
script modules now provide our own argv
printing DB stats only in interactive mode; CC flags
fixed propagation bug in db_solver
CAV 2014 database examples
script.ml compiles again
disabling erroneous DEBUG configuration in backend
a few examples
euf_la_arith -> euf_la_arithmetic
better intf for T-solvers; separated mem from db_solver; local theory fixes