• Sylvain Dailler's avatar
    Q817-011 proof - use cvc4 for floats · 517652cd
    Sylvain Dailler authored
    Driver updates and refactoring. Add new floats drivers file.
    
    Also add Clément's old transformation (intended for colibri) for
    elimination of ident/types/etc.
    
    Change-Id: I161612592904ed3700b414c01ccab7944654d4d9
    (cherry picked from commit a82204236d1e73207dbd71b95236757d0eeacfa2)
    
    Conflicts:
    	drivers/cvc4_14.drv
    	drivers/cvc4_15.drv
    	drivers/cvc4_gnatprove.drv
    	drivers/z3_gnatprove.drv
    	drivers/z3_gnatprove_ce.drv
    517652cd
smt-libv2-floats-int_via_bv.gen 793 Bytes