• Sylvain Dailler's avatar
    R515-014 Adapt new cvc4 to ce · 5b98a355
    Sylvain Dailler authored
    This commit adapts the changes made by Florian to the drivers of cvc4 for
    counterexamples (for float with cvc4 version 1.6). It reuses without
    changes the drivers he intended to use.
    I modified the model parser so that it can recognize float models of cvc4.
    
    * drivers/cvc4_16_counterexample.drv
    Added import smt-libv2-floats.gen.
    
    * src/driver/parse_smtv2_model_lexer.mll
    Added a token for float_type.
    
    * src/driver/parse_smtv2_model_parser.mly
    Float_type can be encountered as names in the model but produce nothing.
    
    
    Change-Id: I64b49dd1824138a5d3f98ab046da0fdbc9420e66
    (cherry picked from commit 226d70801ad449fb86d73d35ac07fcfd56b8ba65)
    
    Conflicts:
    	drivers/cvc4_15_counterexample.drv
    	drivers/cvc4_16_counterexample.drv
    	drivers/cvc4_gnatprove_ce.drv
    5b98a355
cvc4_16_counterexample.drv 1.61 KB