projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3051fd4) | patch
Allow for theory combination of strings with nonlinear real arithmetic. (#5111)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Fri, 2 Oct 2020 15:25:29 +0000 (17:25 +0200)
committerGitHub <noreply@github.com>
Fri, 2 Oct 2020 15:25:29 +0000 (17:25 +0200)
commit7f396917c481de7a57782a5daf31992c37d7d964
treeb12de4d27cf82bdad810305f8883c5bf5372e803tree
parent3051fd4ea618348da9a0b856b7bb07fcda027839commit | diff
Allow for theory combination of strings with nonlinear real arithmetic. (#5111)

This PR makes sure that enabling strings and nonlinear real arithmetic at the same time works fine.
Right now, the configuration for strings enforces linear arithmetic if no integers are enabled, in particular for NRA.

Fixed #5109.
src/smt/set_defaults.cpp diff | blob | history