Skip to content

Commit

Permalink
comment out simple proofs unit test
Browse files Browse the repository at this point in the history
Signed-off-by: Nikolaj Bjorner <[email protected]>
  • Loading branch information
NikolajBjorner committed Sep 24, 2024
1 parent 8b81bda commit 2655301
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion src/api/js/src/high-level/high-level.test.ts
Original file line number Diff line number Diff line change
Expand Up @@ -355,7 +355,9 @@ describe('high-level', () => {
});
});

describe('bitvectors', () => {

describe('bitvectors', () => {
/**
it('can do simple proofs', async () => {
const { BitVec, Concat, Implies, isBitVecVal } = api.Context('main');
Expand All @@ -374,6 +376,7 @@ describe('high-level', () => {
await prove(Implies(Concat(x, y).eq(Concat(y, x)), x.eq(y)));
});
**/

it('finds x and y such that: x ^ y - 103 == x * y', async () => {
const { BitVec, isBitVecVal } = api.Context('main');
Expand All @@ -393,6 +396,7 @@ describe('high-level', () => {
});
});


describe('arrays', () => {
it('Example 1', async () => {
const Z3 = api.Context('main');
Expand Down

0 comments on commit 2655301

Please sign in to comment.