simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 11:45:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

normalize proofs

Browse source
This commit is contained in:
Simon Cruanes 2021-07-18 00:11:56 -04:00
parent ed11741122
commit 77e3c15ad7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smtlib/Process.ml
View file

@ -273,7 +273,7 @@ let process_stmt
let atom, pr_atom = Solver.mk_atom_t solver t in let atom, pr_atom = Solver.mk_atom_t solver t in
CCOpt.iter (fun h -> Vec.push h [atom]) hyps; CCOpt.iter (fun h -> Vec.push h [atom]) hyps;
Solver.add_clause solver (IArray.singleton atom) Solver.add_clause solver (IArray.singleton atom)
Proof.(hres_l (assertion t) [p1 pr_atom]); Proof.(nn @@ hres_l (assertion t) [p1 pr_atom]);
E.return() E.return()
| Statement.Stmt_assert_clause c_ts -> | Statement.Stmt_assert_clause c_ts ->