Unexpected result of VALID

[qOEJXOT4]

I am not expecting this formula (http://logicrunch.it.uu.se:4096/~wv/princess/?ex=perma%2F1681311035_1997373393) to be valid since its basically A & !A for me:

\existentialConstants {
  int a;
}

\problem {
  \exists int v0; (a=(-2*v0)) & ! \exists int v0; (a=(-2*v0))
}

But the Princess Web Interface returns:

VALID

Equivalent constraint:
\forall int v0; a != -2*v0 & \exists int v0; a = -2*v0

Concrete witness:
false

VALID means for me that the formula is true in all interpretations. I don't see how this can be true for this formula.

If I only toggle on +incremental and +model but not +mostGeneralConstraint then the answer is:

VALID

Under the assignment:
sc_5_0_0 = 0

but I cannot interpret this answer and haven't found something similar in the examples.

I would really appreciate if someone could explain the results of Princess to me.

[pruemmer]

This was indeed a bug: a corner case in which Princess first determined that the input formula is quantifier-free (because the quantifiers just encode divisibility), but later preprocessing changed the formula in such a way that it contained "proper" quantifiers. This should now be fixed on master, and in the web interface!

[qOEJXOT4]

@pruemmer Thanks for fixing the bug. I am using princess as a Java Library and need the fixed version of princess for referencing it as a dependency in my project. Unfortunately I was unable to mvn install princess myself.

I did use the scripts from https://central.sonatype.com/artifact/io.github.uuverifiers/princess-parser_2.12/2023-04-07/overview and removed the <scm>-tag in order to use the files of the local cloned repository. Maven clean install resulted in [WARNING] JAR will be empty - no content was marked for inclusion! though.

Can you please tell me how to mvn install princess by using the cloned version of the project? If this is not possible, then publishing the newest version to maven central would help me aswell.

[pruemmer]

I'm planning to publish the next release on Maven central next week.

In the meantime, could you use the version published on our local server?

http://logicrunch.research.it.uu.se/maven/uuverifiers/princess_2.11/

The pom.xml entries for this should be something like:

uuverifiers princess_2.11 2023-05-27 uuverifiers uuverifiers http://logicrunch.research.it.uu.se/maven/

[qOEJXOT4]

Thank you for the quick response. This worked for me.