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

fix(smt): sign error in literal

Browse source
This commit is contained in:
Simon Cruanes 2022-09-10 21:45:43 -04:00
parent 7876820d4d
commit fd39a414c3
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/solver_internal.ml
View file

@ -196,15 +196,15 @@ module Perform_delayed (A : PERFORM_ACTS) = struct
Preprocess.simplify_and_preproc_lit self.preprocess
(preprocess_acts self) lit
in
let t = Lit.term lit in
find_foreign_vars_in_lit self lit;
CC.set_as_lit self.cc (CC.add_term self.cc t) lit;
(let t = Lit.term lit in
CC.set_as_lit self.cc (CC.add_term self.cc t) (Lit.abs lit));
A.add_lit self acts ?default_pol lit
| DA_add_preprocessed_lit { default_pol; lit } ->
let t = Lit.term lit in
Log.debugf 5 (fun k ->
k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp t);
CC.set_as_lit self.cc (CC.add_term self.cc t) lit;
CC.set_as_lit self.cc (CC.add_term self.cc t) (Lit.abs lit);
A.add_lit self acts ?default_pol lit
done
end