multiset_solver cannot even solve trivial goals
I am not sure what goals multiset_solver is supposed to be able to handle, but so far it has solved zero of the goals I tried it on. Here is a rather simple example that only requires reasoning up to A/C:
net_phys, net_ghost : gmultiset val
m : val
-----------------------------------------
{[m]} ⊎ net_ghost ∖ {[m]} ⊎ net_phys = net_ghost ∖ {[m]} ⊎ (net_phys ⊎ {[m]})
Edited by Ralf Jung