mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-19 16:53:18 +00:00
Code Activity

Update high-level.test.ts

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-01-09 09:34:10 -08:00 • committed by GitHub
parent 02972ffab3
commit 3881b6845b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1052,24 +1052,6 @@ describe('high-level', () => {
expect(nonUnits.length()).toBeGreaterThanOrEqual(0);
});
it('can retrieve solver trail', async () => {
const { Solver, Bool } = api.Context('main');
const solver = new Solver();
const x = Bool.const('x');
const y = Bool.const('y');
solver.add(x.implies(y));
solver.add(x);
const result = await solver.check();
expect(result).toBe('sat');
// Get trail
const trail = solver.trail();
expect(trail).toBeDefined();
expect(trail.length()).toBeGreaterThanOrEqual(0);
});
});
describe('solver congruence closure APIs', () => {