mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 18:36:16 +00:00
Code Activity

Fix rcf test

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-28 15:26:48 -08:00
parent 0eea0bea9a
commit 4a57050380
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/test/rcf.cpp
View file

@ -32,7 +32,7 @@ static void tst1() {
#endif #endif
scoped_rcnumeral eps(m); scoped_rcnumeral eps(m);
m.mk_infinitesimal("eps", eps); m.mk_infinitesimal(eps);
mpq aux; mpq aux;
qm.set(aux, 1, 3); qm.set(aux, 1, 3);
m.set(a, aux); m.set(a, aux);
@ -151,7 +151,7 @@ static void tst_denominators() {
scoped_rcnumeral eps(m); scoped_rcnumeral eps(m);
m.mk_pi(a); m.mk_pi(a);
m.inv(a); m.inv(a);
m.mk_infinitesimal("eps", eps); m.mk_infinitesimal(eps);
t = (a - eps*2) / (a*eps + 1); t = (a - eps*2) / (a*eps + 1);
// t = t + a * 2; // t = t + a * 2;
scoped_rcnumeral n(m), d(m); scoped_rcnumeral n(m), d(m);