[Vulkan] Core dump (segfault) with Yices2 solver when `--smtlib2=true` is enabled

[tonghaining]

When using the yices2 solver with the --smtlib2=true flag on the ticketlock-2.1.1.spvasm input (configured with a 2.1.3 thread grid), Dartagnan crashes with a core dump (return code 139, indicating a memory access violation):

$ java -jar dartagnan/target/dartagnan.jar dartagnan/src/test/resources/spirv/vulkan/benchmarks/ticketlock-2.1.1.spvasm cat/vulkan.cat --property=cat_spec --target=vulkan --solver=yices2 --smtlib2=true
Segmentation fault (core dumped)

The crash happens very quickly while there is still plenty of memory available.

The error goes away when disable --smtlib2 or switch to the z3 solver.

[hernanponcedeleon]

In which platform are you trying this?

I cannot reproduce on Linux-x86

> java -jar dartagnan/target/dartagnan.jar dartagnan/src/test/resources/spirv/vulkan/benchmarks/ticketlock-2.1.1.spvasm cat/vulkan.cat --property=cat_spec --target=vulkan --solver=yices2 --smtlib2=true
Test: dartagnan/src/test/resources/spirv/vulkan/benchmarks/ticketlock-2.1.1.spvasm
Result: PASS
Time: 0.840 secs

According to JavaSMT, yices2 "might" work on x86-based Windows and MacOS, but I don't think we have ever tried it.

[hernanponcedeleon]

Ok, I did not realize I actually needed to manually change the grid configuration. I can reproduce it now. Will take a look.

[ThomasHaas]

Have you also tried with --method=eager? Maybe it only happens with the lazy solver.

[hernanponcedeleon]

I already tried it, and it is reproducible with both.

IIRC, once dumped to a file, yices generates one line with potentially huge conjunctions, while z3 does small conjunctions per line. I suspect the problem might be related to this

[hernanponcedeleon]

The problem is in this method from ProverWithTracker

    @Override
    public Void addConstraint(BooleanFormula f) throws InterruptedException {
        if(dump()) {
            write(fmgr.dumpFormula(f).toString());
        }
        return prover.addConstraint(f);
    }

Concretely, when we call toString().

I talked with one of the maintainers of javaSMT on Tuesday and he recommended we wait until they finish integrating the latest version of yices2 to see if the problem remains.