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

fix: compute model even if (potentially) new interface eqns are produced

Browse source 
close #19
This commit is contained in:
Simon Cruanes 2023-06-23 10:44:12 -04:00
parent 3ebc532486
commit c35d721c6d
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/solver_internal.ml
View file

@ -460,7 +460,8 @@ let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t)
if new_intf_eqns <> [] then ( if new_intf_eqns <> [] then (
let (module A) = acts in let (module A) = acts in
List.iter (fun lit -> A.add_lit ~default_pol:false lit) new_intf_eqns List.iter (fun lit -> A.add_lit ~default_pol:false lit) new_intf_eqns
) else if not (has_delayed_actions self) then ( );
if not (has_delayed_actions self) then (
(* if theory combination didn't add new clauses, compute a model *) (* if theory combination didn't add new clauses, compute a model *)
let m = mk_model_ self lits in let m = mk_model_ self lits in
self.last_model <- Some m self.last_model <- Some m