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

fix(lia): problems with only integer constants are not incomplete

Browse source
This commit is contained in:
Simon Cruanes 2022-01-11 13:17:01 -05:00
parent 8410a57f1a
commit 44af0afd59
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/lia/Sidekick_arith_lia.ml
View file

@ -42,7 +42,10 @@ module Make(A : ARG) : S with module A = A = struct
let st = create ~stat (SI.proof si) (SI.tst si) (SI.ty_st si) in
SI.on_preprocess si (fun _si _ t ->
if A.has_ty_int t then (
let is_int_const t = match A.view_as_lia t with
| LIA_const _ -> true | _ -> false in
if A.has_ty_int t && not (is_int_const t) then (
Log.debugf 10 (fun k->k "lia: has ty int %a" T.pp t);
SI.declare_pb_is_incomplete si; (* TODO: remove *)