-
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