mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

fix C(R)

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-09 23:12:55 -07:00
parent ab5894412d
commit f4aae5e56a
2 changed files with 19 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/muz/transforms/dl_mk_separate_negated_tails.cpp
View file

@ -1,3 +1,21 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
mk_separate_negated_tails.cpp
Abstract:
<see header>
Author:
Nikolaj Bjorner (nbjorner) 2013-09-09
Revision History:
--*/
#include "dl_mk_separate_negated_tails.h" #include "dl_mk_separate_negated_tails.h"
#include "dl_context.h" #include "dl_context.h"

5
src/muz/transforms/dl_mk_separate_negated_tails.h
View file

@ -1,5 +1,5 @@
/*++ /*++
Copyright (c) 2006 Microsoft Corporation Copyright (c) 2013 Microsoft Corporation
Module Name: Module Name:
@ -21,9 +21,6 @@ Abstract:
P(x) :- Exists y, z . Q(x,y), !R(y,z), TN(z). P(x) :- Exists y, z . Q(x,y), !R(y,z), TN(z).
TN(z) :- !T(z,u). TN(z) :- !T(z,u).
Author: Author:
Nikolaj Bjorner (nbjorner) 2013-09-09 Nikolaj Bjorner (nbjorner) 2013-09-09