search

kframework / matching-logic-prover

15 stars 4 forks source link

Axiom names are duplicated #52

Open nishantjr opened 4 years ago

nishantjr commented 4 years ago

We've noticed:

    </declaration> <declaration>
      axiom ax1 : functional ( nil_RefDll_t )
    </declaration> <declaration>
      axiom ax1 : heap ( RefDll_t , Dll_t )
    </declaration> <declaration>
      axiom ax2 : \forall { Vfr { RefDll_t } , Vbk { RefDll_t } , Vpr { RefDll_t } , Vnx { RefDll_t } , .Patterns } \iff-lfp ( dll ( Vfr { RefDll_t } , Vbk { RefDll_t } , Vpr { RefDll_t } , Vnx { RefDll_t } , .Patterns ) , \or ( \exists { .Patterns } \and ( \equals ( Vfr { RefDll_t } , Vnx { RefDll_t } ) , \equals ( Vbk { RefDll_t } , Vpr { RefDll_t } ) , emp ( .Patterns ) , .Patterns ) , \exists { Vu { RefDll_t } , .Patterns } \and ( \not ( \equals ( Vfr { RefDll_t } , Vnx { RefDll_t } ) ) , \not ( \equals ( Vbk { RefDll_t } , Vpr { RefDll_t } ) ) , sep ( pto ( Vfr { RefDll_t } , c_Dll_t ( Vu { RefDll_t } , Vpr { RefDll_t } , .Patterns ) , .Patterns ) , dll ( Vu { RefDll_t } , Vbk { RefDll_t } , Vfr { RefDll_t } , Vnx { RefDll_t } , .Patterns ) , .Patterns ) , .Patterns ) , .Patterns ) )
    </declaration> <declaration>
      axiom ax2 : functional ( dll )
    </declaration> <declaration>