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

Fixed uninterpreted predicates for mcsat solver

Browse source
This commit is contained in:
Guillaume Bury 2016-09-23 15:57:38 +02:00
parent 1656995097
commit f35d3a9f23
2 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/mcsat/theory_mcsat.ml
View file

@ -128,7 +128,8 @@ let rec iter_aux f = function
let iter_assignable f = function
| { Expr_smt.atom = Expr_smt.Pred { Expr_smt.term = Expr_smt.Var _ } } -> ()
| { Expr_smt.atom = Expr_smt.Pred { Expr_smt.term = Expr_smt.App (_, _, l) } } ->
| { Expr_smt.atom = Expr_smt.Pred ({ Expr_smt.term = Expr_smt.App (_, _, l) } as t) } ->
if l <> [] then add_watch t (t :: l);
List.iter (iter_aux f) l;
| { Expr_smt.atom = Expr_smt.Equal (a, b) } ->
iter_aux f a; iter_aux f b

2
tests/unsat/test-013.smt2 Normal file
View file

@ -0,0 +1,2 @@
(assert (and (= a b) (not (p a)) (p b)))
(check-sat)