16032530443

Committed 02 Jul 2025 06:08PM UTC coverage: 60.349% (-5.0%) from 65.357%

Build # 16032530443

Build Type

Pull #582

github

Committed by

web-flow

Commit Message

Merge b7e09d316 into b3af64ab1

Pull Request Pull Request #582: Update ci

Coverage Stats

63716 of 105580 relevant lines covered (60.35%)

1127640.75 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

79.38

/src/terms/bvarith64_buffer_terms.c

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

/*
 * BIT-VECTOR OPERATION INVOLVING BUFFERS AND TERMS
 */

#include <assert.h>

#include "terms/bvarith64_buffer_terms.h"
#include "terms/term_utils.h"
#include "utils/int_powers.h"

/*
 * Initialize an auxiliary buffer aux, using the same store and prod table as b
 */
static void init_aux64_buffer(bvarith64_buffer_t *aux, bvarith64_buffer_t *b) {
  init_bvarith64_buffer(aux, b->ptbl, b->store);
  bvarith64_buffer_prepare(aux, b->bitsize);
}

/*
 * Try to convert t to an arithmetic expression
 * - t must be a bv-array term
 * - return true if that succeeds, and store the result in buffer b
 * - otherwise return false and leave b unchanged.
 *
 * We currently just check for the case t = (bvnot x) or t = x.
 * If t is (bvnot x), we store -1 - x in b.
 */
static bool convert_bvarray_to_bvarith64(term_table_t *table, term_t t, bvarith64_buffer_t *b) {
  term_t t0;
  bool negated;

  if (bvarray_convertible_to_term(table, t, &t0, &negated)) {
    if (negated) {
      // t is (bvnot t0) == (-t0) - 1
      bvarith64_buffer_sub_one(b);
      bvarith64_buffer_sub_term(b, table, t0);
    } else {
      bvarith64_buffer_add_term(b, table, t0);
    }
    bvarith64_buffer_normalize(b);
    return true;
  }

  return false;
}


/*
 * Copy t's value into buffer b
 * - t must be defined in table and be a bitvector term
 * - b->ptbl must be the same as table->pprods
 */
void bvarith64_buffer_set_term(bvarith64_buffer_t *b, term_table_t *table, term_t t) {
  uint32_t n;

  assert(b->ptbl == table->pprods);
  assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t));

  n = term_bitsize(table, t);
  bvarith64_buffer_prepare(b, n); // reset b
  bvarith64_buffer_add_term(b, table, t);
}


/*
 * Add t to buffer b
 * - t must be defined in table and be a bitvector term of same bitsize as b
 * - b->ptbl must be the same as table->pprods
 */
void bvarith64_buffer_add_term(bvarith64_buffer_t *b, term_table_t *table, term_t t) {
  pprod_t **v;
  bvpoly64_t *p;
  int32_t i;
  term_t t0;
  bool negated;

  assert(b->ptbl == table->pprods);
  assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
         term_bitsize(table, t) == b->bitsize);

  i = index_of(t);
  switch (kind_for_idx(table, i)) {
  case POWER_PRODUCT:
    bvarith64_buffer_add_pp(b, pprod_for_idx(table, i));
    break;

  case BV64_CONSTANT:
    bvarith64_buffer_add_const(b, bvconst64_for_idx(table, i)->value);
    break;

  case BV64_POLY:
    p = bvpoly64_for_idx(table, i);
    v = pprods_for_bvpoly64(table, p);
    bvarith64_buffer_add_bvpoly(b, p, v);
    term_table_reset_pbuffer(table);
    break;

  case BV_ARRAY:
    if (bvarray_convertible_to_term(table, t, &t0, &negated)) {
      if (negated) {
        // t is (bvnot t0) == (-t0) - 1
        bvarith64_buffer_sub_one(b);
        bvarith64_buffer_sub_term(b, table, t0);
      } else {
        bvarith64_buffer_add_term(b, table, t0);
      }
    } else {
      bvarith64_buffer_add_var(b, t);
    }
    break;

  default:
    bvarith64_buffer_add_var(b, t);
    break;
  }
}


/*
 * Subtract t from buffer b
 * - t must be defined in table and be a bitvector term of same bitsize as b
 * - b->ptbl must be the same as table->pprods
 */
void bvarith64_buffer_sub_term(bvarith64_buffer_t *b, term_table_t *table, term_t t) {
  pprod_t **v;
  bvpoly64_t *p;
  int32_t i;
  term_t t0;
  bool negated;

  assert(b->ptbl == table->pprods);
  assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
         term_bitsize(table, t) == b->bitsize);

  i = index_of(t);
  switch (kind_for_idx(table, i)) {
  case POWER_PRODUCT:
    bvarith64_buffer_sub_pp(b, pprod_for_idx(table, i));
    break;

  case BV64_CONSTANT:
    bvarith64_buffer_sub_const(b, bvconst64_for_idx(table, i)->value);
    break;

  case BV64_POLY:
    p = bvpoly64_for_idx(table, i);
    v = pprods_for_bvpoly64(table, p);
    bvarith64_buffer_sub_bvpoly(b, p, v);
    term_table_reset_pbuffer(table);
    break;

  case BV_ARRAY:
    if (bvarray_convertible_to_term(table, t, &t0, &negated)) {
      if (negated) {
        // t is (bvnot t0) == (-t0) - 1
        bvarith64_buffer_add_one(b);
        bvarith64_buffer_add_term(b, table, t0);
      } else {
        bvarith64_buffer_sub_term(b, table, t0);
      }
    } else {
      bvarith64_buffer_sub_var(b, t);
    }
    break;

  default:
    bvarith64_buffer_sub_var(b, t);
    break;
  }
}



/*
 * Multiply b by t
 * - t must be defined in table and be a bitvector term of same bitsize as b
 * - b->ptbl must be the same as table->pprods
 */
void bvarith64_buffer_mul_term(bvarith64_buffer_t *b, term_table_t *table, term_t t) {
  bvarith64_buffer_t aux;
  pprod_t **v;
  bvpoly64_t *p;
  int32_t i;

  assert(b->ptbl == table->pprods);
  assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
         term_bitsize(table, t) == b->bitsize);

  i = index_of(t);
  switch (kind_for_idx(table, i)) {
  case POWER_PRODUCT:
    bvarith64_buffer_mul_pp(b, pprod_for_idx(table, i));
    break;

  case BV64_CONSTANT:
    bvarith64_buffer_mul_const(b, bvconst64_for_idx(table, i)->value);
    break;

  case BV64_POLY:
    p = bvpoly64_for_idx(table, i);
    v = pprods_for_bvpoly64(table, p);
    bvarith64_buffer_mul_bvpoly(b, p, v);
    term_table_reset_pbuffer(table);
    break;

  case BV_ARRAY:
    init_aux64_buffer(&aux, b);
    if (convert_bvarray_to_bvarith64(table, t, &aux)) {
      bvarith64_buffer_mul_buffer(b, &aux);
    } else {
      bvarith64_buffer_mul_var(b, t);
    }
    delete_bvarith64_buffer(&aux);
    break;

  default:
    bvarith64_buffer_mul_var(b, t);
    break;
  }
}


/*
 * Add a * t to b
 * - t must be defined in table and be a bitvector term of same bitsize as b
 * - b->ptbl must be the same as table->pprods
 */
void bvarith64_buffer_add_const_times_term(bvarith64_buffer_t *b, term_table_t *table, uint64_t a, term_t t) {
  pprod_t **v;
  bvpoly64_t *p;
  int32_t i;
  term_t t0;
  bool negated;

  assert(b->ptbl == table->pprods);
  assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
         term_bitsize(table, t) == b->bitsize);

  i = index_of(t);
  switch (kind_for_idx(table, i)) {
  case POWER_PRODUCT:
    bvarith64_buffer_add_mono(b, a, pprod_for_idx(table, i));
    break;

  case BV64_CONSTANT:
    a *= bvconst64_for_idx(table, i)->value;
    bvarith64_buffer_add_const(b, a);
    break;

  case BV64_POLY:
    p = bvpoly64_for_idx(table, i);
    v = pprods_for_bvpoly64(table, p);
    bvarith64_buffer_add_const_times_bvpoly(b, p, v, a);
    term_table_reset_pbuffer(table);
    break;

  case BV_ARRAY:
    if (bvarray_convertible_to_term(table, t, &t0, &negated)) {
      if (negated) {
        // t is (bvnot t0) == (-t0) - 1
        bvarith64_buffer_sub_const(b, a);
        bvarith64_buffer_add_const_times_term(b, table, -a, t0);
      } else {
        bvarith64_buffer_add_const_times_term(b, table, a, t0);
      }
    } else {
      bvarith64_buffer_add_varmono(b, a, t);
    }
    break;

  default:
    bvarith64_buffer_add_varmono(b, a, t);
    break;
  }
}


/*
 * Multiply b by t^d
 * - t must be an arithmetic term
 * - p->ptbl and table->pprods must be equal
 */
void bvarith64_buffer_mul_term_power(bvarith64_buffer_t *b, term_table_t *table, term_t t, uint32_t d) {
  bvarith64_buffer_t aux, aux2;
  bvpoly64_t *p;
  pprod_t **v;
  pprod_t *r;
  uint64_t c;
  int32_t i;

  assert(b->ptbl == table->pprods);
  assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
         term_bitsize(table, t) == b->bitsize);

  i = index_of(t);
  switch (kind_for_idx(table, i)) {
  case POWER_PRODUCT:
    r = pprod_exp(b->ptbl, pprod_for_idx(table, i), d); // r = t^d
    bvarith64_buffer_mul_pp(b, r);
    break;

  case BV64_CONSTANT:
    c = upower64(bvconst64_for_idx(table, i)->value, d); // c := t^d
    bvarith64_buffer_mul_const(b, c);
    break;

  case BV64_POLY:
    p = bvpoly64_for_idx(table, i);
    v = pprods_for_bvpoly64(table, p);
    init_aux64_buffer(&aux, b);
    bvarith64_buffer_mul_bvpoly_power(b, p, v, d, &aux);
    delete_bvarith64_buffer(&aux);
    term_table_reset_pbuffer(table);
    break;

  case BV_ARRAY:
    init_aux64_buffer(&aux, b);
    if (convert_bvarray_to_bvarith64(table, t, &aux)) {
      init_aux64_buffer(&aux2, b);
      bvarith64_buffer_mul_buffer_power(b, &aux, d, &aux2);
      delete_bvarith64_buffer(&aux2);
    } else {
      r = pprod_varexp(b->ptbl, t, d);
      bvarith64_buffer_mul_pp(b, r);
    }
    delete_bvarith64_buffer(&aux);
    break;

  default:
    r = pprod_varexp(b->ptbl, t, d);
    bvarith64_buffer_mul_pp(b, r);
    break;
  }
}

1	/*
2	* This file is part of the Yices SMT Solver.
3	* Copyright (C) 2017 SRI International.
4	*
5	* Yices is free software: you can redistribute it and/or modify
6	* it under the terms of the GNU General Public License as published by
7	* the Free Software Foundation, either version 3 of the License, or
8	* (at your option) any later version.
9	*
10	* Yices is distributed in the hope that it will be useful,
11	* but WITHOUT ANY WARRANTY; without even the implied warranty of
12	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13	* GNU General Public License for more details.
14	*
15	* You should have received a copy of the GNU General Public License
16	* along with Yices. If not, see <http://www.gnu.org/licenses/>.
17	*/
18
19	/*
20	* BIT-VECTOR OPERATION INVOLVING BUFFERS AND TERMS
21	*/
22
23	#include <assert.h>
24
25	#include "terms/bvarith64_buffer_terms.h"
26	#include "terms/term_utils.h"
27	#include "utils/int_powers.h"
28
29	/*
30	* Initialize an auxiliary buffer aux, using the same store and prod table as b
31	*/
32	static void init_aux64_buffer(bvarith64_buffer_t aux, bvarith64_buffer_t b) {	264✔
33	init_bvarith64_buffer(aux, b->ptbl, b->store);	264✔
34	bvarith64_buffer_prepare(aux, b->bitsize);	264✔
35	}	264✔
36
37	/*
38	* Try to convert t to an arithmetic expression
39	* - t must be a bv-array term
40	* - return true if that succeeds, and store the result in buffer b
41	* - otherwise return false and leave b unchanged.
42	*
43	* We currently just check for the case t = (bvnot x) or t = x.
44	* If t is (bvnot x), we store -1 - x in b.
45	*/
46	static bool convert_bvarray_to_bvarith64(term_table_t table, term_t t, bvarith64_buffer_t b) {	264✔
47	term_t t0;
48	bool negated;
49
50	if (bvarray_convertible_to_term(table, t, &t0, &negated)) {	264✔
51	if (negated) {	1✔
52	// t is (bvnot t0) == (-t0) - 1
53	bvarith64_buffer_sub_one(b);	1✔
54	bvarith64_buffer_sub_term(b, table, t0);	1✔
55	} else {
56	bvarith64_buffer_add_term(b, table, t0);	×
57	}
58	bvarith64_buffer_normalize(b);	1✔
59	return true;	1✔
60	}
61
62	return false;	263✔
63	}
64
65
66	/*
67	* Copy t's value into buffer b
68	* - t must be defined in table and be a bitvector term
69	* - b->ptbl must be the same as table->pprods
70	*/
71	void bvarith64_buffer_set_term(bvarith64_buffer_t b, term_table_t table, term_t t) {	×
72	uint32_t n;
73
74	assert(b->ptbl == table->pprods);
75	assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t));
76
77	n = term_bitsize(table, t);	×
78	bvarith64_buffer_prepare(b, n); // reset b	×
79	bvarith64_buffer_add_term(b, table, t);	×
80	}	×
81
82
83	/*
84	* Add t to buffer b
85	* - t must be defined in table and be a bitvector term of same bitsize as b
86	* - b->ptbl must be the same as table->pprods
87	*/
88	void bvarith64_buffer_add_term(bvarith64_buffer_t b, term_table_t table, term_t t) {	6,556✔
89	pprod_t **v;
90	bvpoly64_t *p;
91	int32_t i;
92	term_t t0;
93	bool negated;
94
95	assert(b->ptbl == table->pprods);
96	assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
97	term_bitsize(table, t) == b->bitsize);
98
99	i = index_of(t);	6,556✔
100	switch (kind_for_idx(table, i)) {	6,556✔
101	case POWER_PRODUCT:	8✔
102	bvarith64_buffer_add_pp(b, pprod_for_idx(table, i));	8✔
103	break;	8✔
104
105	case BV64_CONSTANT:	538✔
106	bvarith64_buffer_add_const(b, bvconst64_for_idx(table, i)->value);	538✔
107	break;	538✔
108
109	case BV64_POLY:	2,418✔
110	p = bvpoly64_for_idx(table, i);	2,418✔
111	v = pprods_for_bvpoly64(table, p);	2,418✔
112	bvarith64_buffer_add_bvpoly(b, p, v);	2,418✔
113	term_table_reset_pbuffer(table);	2,418✔
114	break;	2,418✔
115
116	case BV_ARRAY:	1,154✔
117	if (bvarray_convertible_to_term(table, t, &t0, &negated)) {	1,154✔
118	if (negated) {	30✔
119	// t is (bvnot t0) == (-t0) - 1
120	bvarith64_buffer_sub_one(b);	30✔
121	bvarith64_buffer_sub_term(b, table, t0);	30✔
122	} else {
123	bvarith64_buffer_add_term(b, table, t0);	×
124	}
125	} else {
126	bvarith64_buffer_add_var(b, t);	1,124✔
127	}
128	break;	1,154✔
129
130	default:	2,438✔
131	bvarith64_buffer_add_var(b, t);	2,438✔
132	break;	2,438✔
133	}
134	}	6,556✔
135
136
137	/*
138	* Subtract t from buffer b
139	* - t must be defined in table and be a bitvector term of same bitsize as b
140	* - b->ptbl must be the same as table->pprods
141	*/
142	void bvarith64_buffer_sub_term(bvarith64_buffer_t b, term_table_t table, term_t t) {	755✔
143	pprod_t **v;
144	bvpoly64_t *p;
145	int32_t i;
146	term_t t0;
147	bool negated;
148
149	assert(b->ptbl == table->pprods);
150	assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
151	term_bitsize(table, t) == b->bitsize);
152
153	i = index_of(t);	755✔
154	switch (kind_for_idx(table, i)) {	755✔
155	case POWER_PRODUCT:	8✔
156	bvarith64_buffer_sub_pp(b, pprod_for_idx(table, i));	8✔
157	break;	8✔
158
159	case BV64_CONSTANT:	99✔
160	bvarith64_buffer_sub_const(b, bvconst64_for_idx(table, i)->value);	99✔
161	break;	99✔
162
163	case BV64_POLY:	94✔
164	p = bvpoly64_for_idx(table, i);	94✔
165	v = pprods_for_bvpoly64(table, p);	94✔
166	bvarith64_buffer_sub_bvpoly(b, p, v);	94✔
167	term_table_reset_pbuffer(table);	94✔
168	break;	94✔
169
170	case BV_ARRAY:	324✔
171	if (bvarray_convertible_to_term(table, t, &t0, &negated)) {	324✔
172	if (negated) {	5✔
173	// t is (bvnot t0) == (-t0) - 1
174	bvarith64_buffer_add_one(b);	5✔
175	bvarith64_buffer_add_term(b, table, t0);	5✔
176	} else {
177	bvarith64_buffer_sub_term(b, table, t0);	×
178	}
179	} else {
180	bvarith64_buffer_sub_var(b, t);	319✔
181	}
182	break;	324✔
183
184	default:	230✔
185	bvarith64_buffer_sub_var(b, t);	230✔
186	break;	230✔
187	}
188	}	755✔
189
190
191
192	/*
193	* Multiply b by t
194	* - t must be defined in table and be a bitvector term of same bitsize as b
195	* - b->ptbl must be the same as table->pprods
196	*/
197	void bvarith64_buffer_mul_term(bvarith64_buffer_t b, term_table_t table, term_t t) {	773✔
198	bvarith64_buffer_t aux;
199	pprod_t **v;
200	bvpoly64_t *p;
201	int32_t i;
202
203	assert(b->ptbl == table->pprods);
204	assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
205	term_bitsize(table, t) == b->bitsize);
206
207	i = index_of(t);	773✔
208	switch (kind_for_idx(table, i)) {	773✔
209	case POWER_PRODUCT:	8✔
210	bvarith64_buffer_mul_pp(b, pprod_for_idx(table, i));	8✔
211	break;	8✔
212
213	case BV64_CONSTANT:	36✔
214	bvarith64_buffer_mul_const(b, bvconst64_for_idx(table, i)->value);	36✔
215	break;	36✔
216
217	case BV64_POLY:	15✔
218	p = bvpoly64_for_idx(table, i);	15✔
219	v = pprods_for_bvpoly64(table, p);	15✔
220	bvarith64_buffer_mul_bvpoly(b, p, v);	15✔
221	term_table_reset_pbuffer(table);	15✔
222	break;	15✔
223
224	case BV_ARRAY:	166✔
225	init_aux64_buffer(&aux, b);	166✔
226	if (convert_bvarray_to_bvarith64(table, t, &aux)) {	166✔
227	bvarith64_buffer_mul_buffer(b, &aux);	1✔
228	} else {
229	bvarith64_buffer_mul_var(b, t);	165✔
230	}
231	delete_bvarith64_buffer(&aux);	166✔
232	break;	166✔
233
234	default:	548✔
235	bvarith64_buffer_mul_var(b, t);	548✔
236	break;	548✔
237	}
238	}	773✔
239
240
241	/*
242	* Add a * t to b
243	* - t must be defined in table and be a bitvector term of same bitsize as b
244	* - b->ptbl must be the same as table->pprods
245	*/
246	void bvarith64_buffer_add_const_times_term(bvarith64_buffer_t b, term_table_t table, uint64_t a, term_t t) {	24,978✔
247	pprod_t **v;
248	bvpoly64_t *p;
249	int32_t i;
250	term_t t0;
251	bool negated;
252
253	assert(b->ptbl == table->pprods);
254	assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
255	term_bitsize(table, t) == b->bitsize);
256
257	i = index_of(t);	24,978✔
258	switch (kind_for_idx(table, i)) {	24,978✔
259	case POWER_PRODUCT:	1✔
260	bvarith64_buffer_add_mono(b, a, pprod_for_idx(table, i));	1✔
261	break;	1✔
262
263	case BV64_CONSTANT:	14,418✔
264	a *= bvconst64_for_idx(table, i)->value;	14,418✔
265	bvarith64_buffer_add_const(b, a);	14,418✔
266	break;	14,418✔
267
268	case BV64_POLY:	×
269	p = bvpoly64_for_idx(table, i);	×
270	v = pprods_for_bvpoly64(table, p);	×
271	bvarith64_buffer_add_const_times_bvpoly(b, p, v, a);	×
272	term_table_reset_pbuffer(table);	×
273	break;	×
274
275	case BV_ARRAY:	643✔
276	if (bvarray_convertible_to_term(table, t, &t0, &negated)) {	643✔
277	if (negated) {	×
278	// t is (bvnot t0) == (-t0) - 1
279	bvarith64_buffer_sub_const(b, a);	×
280	bvarith64_buffer_add_const_times_term(b, table, -a, t0);	×
281	} else {
282	bvarith64_buffer_add_const_times_term(b, table, a, t0);	×
283	}
284	} else {
285	bvarith64_buffer_add_varmono(b, a, t);	643✔
286	}
287	break;	643✔
288
289	default:	9,916✔
290	bvarith64_buffer_add_varmono(b, a, t);	9,916✔
291	break;	9,916✔
292	}
293	}	24,978✔
294
295
296	/*
297	* Multiply b by t^d
298	* - t must be an arithmetic term
299	* - p->ptbl and table->pprods must be equal
300	*/
301	void bvarith64_buffer_mul_term_power(bvarith64_buffer_t b, term_table_t table, term_t t, uint32_t d) {	126✔
302	bvarith64_buffer_t aux, aux2;
303	bvpoly64_t *p;
304	pprod_t **v;
305	pprod_t *r;
306	uint64_t c;
307	int32_t i;
308
309	assert(b->ptbl == table->pprods);
310	assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
311	term_bitsize(table, t) == b->bitsize);
312
313	i = index_of(t);	126✔
314	switch (kind_for_idx(table, i)) {	126✔
315	case POWER_PRODUCT:	×
316	r = pprod_exp(b->ptbl, pprod_for_idx(table, i), d); // r = t^d	×
317	bvarith64_buffer_mul_pp(b, r);	×
318	break;	×
319
320	case BV64_CONSTANT:	26✔
321	c = upower64(bvconst64_for_idx(table, i)->value, d); // c := t^d	26✔
322	bvarith64_buffer_mul_const(b, c);	26✔
323	break;	26✔
324
325	case BV64_POLY:	×
326	p = bvpoly64_for_idx(table, i);	×
327	v = pprods_for_bvpoly64(table, p);	×
328	init_aux64_buffer(&aux, b);	×
329	bvarith64_buffer_mul_bvpoly_power(b, p, v, d, &aux);	×
330	delete_bvarith64_buffer(&aux);	×
331	term_table_reset_pbuffer(table);	×
332	break;	×
333
334	case BV_ARRAY:	98✔
335	init_aux64_buffer(&aux, b);	98✔
336	if (convert_bvarray_to_bvarith64(table, t, &aux)) {	98✔
337	init_aux64_buffer(&aux2, b);	×
338	bvarith64_buffer_mul_buffer_power(b, &aux, d, &aux2);	×
339	delete_bvarith64_buffer(&aux2);	×
340	} else {
341	r = pprod_varexp(b->ptbl, t, d);	98✔
342	bvarith64_buffer_mul_pp(b, r);	98✔
343	}
344	delete_bvarith64_buffer(&aux);	98✔
345	break;	98✔
346
347	default:	2✔
348	r = pprod_varexp(b->ptbl, t, d);	2✔
349	bvarith64_buffer_mul_pp(b, r);	2✔
350	break;	2✔
351	}
352	}	126✔

SRI-CSL / yices2 / 16032530443

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous