mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

wasm: increase timeout in tests (#7401)

Browse source
This commit is contained in:
Kevin Gibbons 2024-09-25 10:33:14 -07:00 committed by GitHub
parent 103c5ad71c
commit 77aa5280df
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/js/src/high-level/high-level.test.ts
View file

@ -380,7 +380,7 @@ describe('high-level', () => {
const y = BitVec.const('y', 32); const y = BitVec.const('y', 32);
await prove(Implies(Concat(x, y).eq(Concat(y, x)), x.eq(y))); await prove(Implies(Concat(x, y).eq(Concat(y, x)), x.eq(y)));
}); }, 10_000 /* timeout ms */);
it('finds x and y such that: x ^ y - 103 == x * y', async () => { it('finds x and y such that: x ^ y - 103 == x * y', async () => {
const { BitVec, isBitVecVal } = api.Context('main'); const { BitVec, isBitVecVal } = api.Context('main');
@ -455,7 +455,7 @@ describe('high-level', () => {
await prove(Eq(arr2.select(0), FIVE_VAL)); await prove(Eq(arr2.select(0), FIVE_VAL));
await prove(Not(Eq(arr2.select(0), BitVec.val(6, 256)))); await prove(Not(Eq(arr2.select(0), BitVec.val(6, 256))));
await prove(Eq(arr2.store(idx, val).select(idx), constArr.store(idx, val).select(idx))); await prove(Eq(arr2.store(idx, val).select(idx), constArr.store(idx, val).select(idx)));
}); }, 10_000 /* timeout ms */);
it('Finds arrays that differ but that sum to the same', async () => { it('Finds arrays that differ but that sum to the same', async () => {
const Z3 = api.Context('main'); const Z3 = api.Context('main');