projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0f25a37) | patch
Fix non-linear equality solving that involves mixed real/integer arithmetic (#3739)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 12 Feb 2020 00:20:25 +0000 (18:20 -0600)
committerGitHub <noreply@github.com>
Wed, 12 Feb 2020 00:20:25 +0000 (16:20 -0800)
commit0858188716609ae8a45e542bc4e054e675f2676d
tree82f206b79dc8f7f1235d79cb3e8da73187f28c86tree
parent0f25a37b05db224fe16c3c0357c24d89ad9e5ceecommit | diff
Fix non-linear equality solving that involves mixed real/integer arithmetic (#3739)

* Fix non-linear equality solving that involves mixed real/integer.

* Format

* Fix

* Revert

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
src/theory/arith/nl_model.cpp diff | blob | history