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

add basic test for th-cstor

Browse source
This commit is contained in:
Simon Cruanes 2019-11-19 19:48:09 -06:00
parent e414112010
commit f1fc429b5a
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/th-cstor/Sidekick_th_cstor.ml
View file

@ -46,6 +46,9 @@ module Make(A : ARG) : S with module A = A = struct
let on_new_term self _solver n (t:T.t) = let on_new_term self _solver n (t:T.t) =
match A.view_as_cstor t with match A.view_as_cstor t with
| T_cstor (cstor,args) -> | T_cstor (cstor,args) ->
Log.debugf 20
(fun k->k "(@[th-cstor.on-new-term@ %a@ :cstor %a@ @[:args@ (@[%a@])@]@]@])"
T.pp t Fun.pp cstor (Util.pp_iarray T.pp) args);
N_tbl.add self.cstors n {n; t; cstor; args}; N_tbl.add self.cstors n {n; t; cstor; args};
| _ -> () | _ -> ()

6
tests/unsat/cstor1.smt2 Normal file
View file

@ -0,0 +1,6 @@
(set-info :status unsat)
(declare-datatypes ((nat 0)) (((succ (pred nat)) (zero))))
(assert (= (succ (succ zero)) (succ zero)))
(check-sat)