mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-01 14:47:51 +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
parent 6b3adcf259
commit 617fb60176
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); 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', () => { describe('solver congruence closure APIs', () => {