fixing stupidity in yices translation (add, mul)

SRI-CSL · Apr 15, 2016 · 9738ede · 9738ede
1 parent d995eed
commit 9738ede
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/smt/yices2/yices2_internal.cpp b/src/smt/yices2/yices2_internal.cpp
@@ -169,7 +169,7 @@ term_t yices2_internal::mk_yices2_term(expr::term_op op, size_t n, term_t* child
   case expr::TERM_BV_ADD: {
     assert(n >= 2);
     result = yices_bvadd(children[0], children[1]);
-    for (size_t i = 3; i < n; ++ i) {
+    for (size_t i = 2; i < n; ++ i) {
       result = yices_bvadd(result, children[i]);
     }
     break;
@@ -184,7 +184,7 @@ term_t yices2_internal::mk_yices2_term(expr::term_op op, size_t n, term_t* child
   case expr::TERM_BV_MUL: {
     assert(n >= 2);
     result = yices_bvmul(children[0], children[1]);
-    for (size_t i = 3; i < n; ++ i) {
+    for (size_t i = 2; i < n; ++ i) {
       result = yices_bvmul(result, children[i]);
     }
     break;