projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a7ddc49) | patch
Merging in a fix from 1.3.x.
authorTim King <taking@cs.nyu.edu>
Wed, 26 Mar 2014 20:56:13 +0000 (16:56 -0400)
committerTim King <taking@cs.nyu.edu>
Wed, 26 Mar 2014 20:58:45 +0000 (16:58 -0400)
commit1cadb3c1034a9a5b0a778b25769ab1a8101de4f1
treef1e406220b57165ad249b8b1a3736804459a0605tree
parenta7ddc4951cf38434062f02afd59340355f157b8fcommit | diff
Merging in a fix from 1.3.x.
Fixes an idempotency issue for non-linear multiplication with integer and real variables.

Conflicts:
src/theory/arith/normal_form.cpp
src/theory/arith/normal_form.cpp diff | blob | history
src/theory/arith/normal_form.h diff | blob | history