Problem with modulo method in yices2

[hernanponcedeleon]

As I commented in 90e309f03cf194f15cbdcc528e4f079b9164a56a, I am seeing a regression in version 5.0.0 related to the modulo method for the yices2 solver.

@baierd we are using JavaSMT as a backend of our verifier, but here is self-contained test that reproduces the problem and the stack trace

public class JavaSMT {

    @Test
    public void test() throws Exception {

        Configuration solverConfig = Configuration.builder().build();

        try (SolverContext context = SolverContextFactory.createSolverContext(solverConfig, BasicLogManager.create(solverConfig), ShutdownManager.create().getNotifier(), Solvers.YICES2)) {
            BitvectorFormulaManager bvmgr = context.getFormulaManager().getBitvectorFormulaManager();

            BitvectorFormula a = bvmgr.makeBitvector(1, 0);
            BitvectorFormula b = bvmgr.makeBitvector(1, 1);
            BitvectorFormula m = bvmgr.modulo(a, b, true);
            BooleanFormula f = bvmgr.equal(m, a);

            try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
                prover.addConstraint(f);
                boolean isUnsat = prover.isUnsat();
                assert !isUnsat;
                try (Model model = prover.getModel()) {
                    System.out.printf("Done");
                }   
            }
        }
    }
}

...

java.lang.AbstractMethodError: Receiver class org.sosy_lab.java_smt.solvers.yices2.Yices2BitvectorFormulaManager does not define or inherit an implementation of the resolved method 'abstract java.lang.Object remainder(java.lang.Object, java.lang.Object, boolean)' of abstract class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager.
        at org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager.remainder(AbstractBitvectorFormulaManager.java:123)
        at org.sosy_lab.java_smt.api.BitvectorFormulaManager.modulo(BitvectorFormulaManager.java:138)
        at com.dat3m.dartagnan.exceptions.JavaSMT.test(JavaSMT.java:30)
        at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
        at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:77)
        at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
        at java.base/java.lang.reflect.Method.invoke(Method.java:568)
        at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:59)
        at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
        at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:56)
        at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
        at org.junit.runners.ParentRunner$3.evaluate(ParentRunner.java:306)
        at org.junit.runners.BlockJUnit4ClassRunner$1.evaluate(BlockJUnit4ClassRunner.java:100)
        at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:366)
        at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:103)
        at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:63)
        at org.junit.runners.ParentRunner$4.run(ParentRunner.java:331)
        at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:79)
        at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:329)
        at org.junit.runners.ParentRunner.access$100(ParentRunner.java:66)
        at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:293)
        at org.junit.runners.ParentRunner$3.evaluate(ParentRunner.java:306)
        at org.junit.runners.ParentRunner.run(ParentRunner.java:413)
        at org.apache.maven.surefire.junit4.JUnit4Provider.execute(JUnit4Provider.java:316)
        at org.apache.maven.surefire.junit4.JUnit4Provider.executeWithRerun(JUnit4Provider.java:240)
        at org.apache.maven.surefire.junit4.JUnit4Provider.executeTestSet(JUnit4Provider.java:214)
        at org.apache.maven.surefire.junit4.JUnit4Provider.invoke(JUnit4Provider.java:155)
        at org.apache.maven.surefire.booter.ForkedBooter.runSuitesInProcess(ForkedBooter.java:385)
        at org.apache.maven.surefire.booter.ForkedBooter.execute(ForkedBooter.java:162)
        at org.apache.maven.surefire.booter.ForkedBooter.run(ForkedBooter.java:507)
        at org.apache.maven.surefire.booter.ForkedBooter.main(ForkedBooter.java:495)

And here you can see our pom.xml configuration with the concrete versions of the libraries.

[kfriedberger]

Ah sorry, that issue might be an old problem again: We did an API-change in JavaSMT and did not fully update the Yices bindings.

A developer for JavaSMT can not find this issue "within" JavaSMT, because the problem only exists when using (sligthly) incompatible or outdated libraries. I will publish the correct version soon.

[kfriedberger]

I had another look, and "we" (JavaSMT) had already updated the Yices bindings correctly when releasing JavaSMT 5.0.0. Hurray.

However, @hernanponcedeleon : The version for Dat3M does reference an older version here: https://github.com/hernanponcedeleon/Dat3M/blob/087b33a9324e3493575f7d4e6ae097e2eba8eb6d/pom.xml#L40 and that version is (sligthly) incompatible with JavaSMT 5.0.0. Please take a look at our example pom-file and update your version accordingly: https://github.com/sosy-lab/java-smt/commit/1d4cc82cc6b10ce7897b277d69f8eda7a8f3b275#diff-cece5ce08db89151fb3824cb13cec67361f8af0cdee4b5d09302964fa504725eR79

:smile:

[hernanponcedeleon]

My bad ... I used the release notes to figure out which solvers changed. I did not notice the update to javasmt-yices.version even if yices.version did not change.

Thanks @kfriedberger for taking a look.

[kfriedberger]

@hernanponcedeleon please consider the following hint:

Yices2 is licensed under GPL and therefore cannot be combined with software under different licenses like Apache 2.0. JavaSMT does not include its Yices2 bindings as part of its main library. The same rule might apply to Dat3M.