Change bvudiv semantics based on input language (#1292)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sat, 28 Oct 2017 23:45:16 +0000 (16:45 -0700)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 28 Oct 2017 23:45:16 +0000 (18:45 -0500)
commita5c79c991506610e47a8f503a2b775aa4b5fa63f
tree7f5cbdf9294407219dec181e3ba99fc6294677e0
parentd33fc58a4fccfe6bc9059e0dd47afea2ed69d1ad
Change bvudiv semantics based on input language (#1292)

* Change bvudiv semantics based on input language

The semantics of division by zero have changed from SMT 2.5 to SMT 2.6.
This commit sets the default options for the division semantics based on
the language version used. The input language was already kept track of
in the options, so this commit just updates the input language option
when there is a set-info command. This mirrors how the code already
deals with the output language.

Note: With this commit, set-info overwrites the option set by the user.
This is done to be consistent with the parser.

This partially fixes #1241.

* clang format
src/smt/smt_engine.cpp
test/regress/regress0/bv/Makefile.am
test/regress/regress0/bv/divtest_2_5.smt2 [new file with mode: 0644]
test/regress/regress0/bv/divtest_2_6.smt2 [new file with mode: 0644]