java-smt icon indicating copy to clipboard operation
java-smt copied to clipboard

Published 20 hours ago • verified publisher icon sosy-lab

ProverEnvironment pop Later, the variable will be incorrectly modified to be invalid argument. Z3

Open yupengj opened this issue 1 year ago • 1 comments

code

    @Test
    void push_pop_test() throws InterruptedException{
        SolverContext solverContext = SmtSolverUtil.solverContext();
        FormulaManager formulaManager = solverContext.getFormulaManager();
        ProverEnvironment prover = SmtSolverUtil.prover(solverContext);
        IntegerFormulaManager integerFormulaManager = formulaManager.getIntegerFormulaManager();

        // constraint: F1>=10
        NumeralFormula.IntegerFormula integerFormula = integerFormulaManager.makeVariable("F1");
        BooleanFormula booleanFormula = integerFormulaManager.greaterThan(integerFormula, integerFormulaManager.makeNumber(10));
        // add constraint: F1>=10
        prover.addConstraint(booleanFormula);

        // add other constraints，It's different every time, check if f1=1 satisfies other constraint
        
        // boolean variable: F1=1
        BooleanFormula booleanVar = integerFormulaManager.equal(integerFormula, integerFormulaManager.makeNumber(1));
        for (int i = 0; i < 10; i++) {
            prover.push();
            prover.addConstraint(booleanVar);
            log.info("booleanVar1:{}", booleanVar); // booleanVar1:(= F1 1)
            prover.pop();
            log.info("booleanVar2:{}", booleanVar); // booleanVar2:(:var 1047405008)
        }
    }

Exception

11:14:54.764 [main] INFO com.gantang.prd.commons.solverengine.javasmt.JavaSmtTest -- booleanVar1:(= F1 1)
11:14:54.764 [main] INFO com.gantang.prd.commons.solverengine.javasmt.JavaSmtTest -- booleanVar2:(:var 767927760)

com.microsoft.z3.Z3Exception: invalid argument

	at com.microsoft.z3.Native.solverAssertAndTrack(Native.java:5051)
	at org.sosy_lab.java_smt.solvers.z3.Z3TheoremProver.assertContraintAndTrack(Z3TheoremProver.java:78)
	at org.sosy_lab.java_smt.solvers.z3.Z3AbstractProver.addConstraintImpl(Z3AbstractProver.java:134)
	at org.sosy_lab.java_smt.solvers.z3.Z3AbstractProver.addConstraintImpl(Z3AbstractProver.java:40)
	at org.sosy_lab.java_smt.basicimpl.AbstractProver.addConstraint(AbstractProver.java:108)
	at com.gantang.prd.commons.solverengine.javasmt.JavaSmtTest.push_pop_test(JavaSmtTest.java:214)
	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.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:727)
	at org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
	at org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
	at org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:156)
	at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:147)
	at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestMethod(TimeoutExtension.java:86)
	at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(InterceptingExecutableInvoker.java:103)
	at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.lambda$invoke$0(InterceptingExecutableInvoker.java:93)
	at org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
	at org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
	at org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
	at org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
	at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:92)
	at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:86)
	at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$7(TestMethodTestDescriptor.java:217)
	at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:213)
	at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138)
	at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:151)
	at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141)
	at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139)
	at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95)
	at java.base/java.util.ArrayList.forEach(ArrayList.java:1511)
	at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:155)
	at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141)
	at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139)
	at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95)
	at java.base/java.util.ArrayList.forEach(ArrayList.java:1511)
	at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:155)
	at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141)
	at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139)
	at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95)
	at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
	at org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
	at org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
	at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:147)
	at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:127)
	at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:90)
	at org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:55)
	at org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:102)
	at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:54)
	at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
	at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
	at org.junit.platform.launcher.core.DefaultLauncherSession$DelegatingLauncher.execute(DefaultLauncherSession.java:86)
	at org.junit.platform.launcher.core.SessionPerRequestLauncher.execute(SessionPerRequestLauncher.java:53)
	at com.intellij.junit5.JUnit5IdeaTestRunner.startRunnerWithArgs(JUnit5IdeaTestRunner.java:57)
	at com.intellij.rt.junit.IdeaTestRunner$Repeater$1.execute(IdeaTestRunner.java:38)
	at com.intellij.rt.execution.junit.TestsRepeater.repeat(TestsRepeater.java:11)
	at com.intellij.rt.junit.IdeaTestRunner$Repeater.startRunnerWithArgs(IdeaTestRunner.java:35)
	at com.intellij.rt.junit.JUnitStarter.prepareStreamsAndStart(JUnitStarter.java:232)
	at com.intellij.rt.junit.JUnitStarter.main(JUnitStarter.java:55)

version : api "org.sosy-lab:java-smt:4.1.0" api group: 'org.sosy-lab', name: 'javasmt-solver-z3', version: '4.12.2', classifier: 'com.microsoft.z3', ext: 'jar'

I have no problem writing the same logic using the z3 Java API

@Test
    void test_z3() {
        // load z3 library
        SolverContext solverContext = SmtSolverUtil.solverContext();
        Context ctx = new Context();
        try {
            IntExpr f1 = ctx.mkIntConst("f1");
            IntNum intNum = ctx.mkInt(10);
            // constraint： f1>=10
            BoolExpr constraint = ctx.mkGe(f1, intNum);
            Solver solver = ctx.mkSolver();
            //add constraint： f1>=10
            solver.add(constraint);

            solver.push();
            IntNum intNum1 = ctx.mkInt(1);
            BoolExpr equal = ctx.mkEq(f1, intNum1);

            for (int i = 0; i < 10; i++) {
                solver.push();
                log.info("equal:{}", equal);
                solver.add(equal);
                Status result = solver.check();
                log.info("result:{}", result);
                solver.pop();
            }
            solver.pop();
        } finally {
            // 清理上下文资源
            ctx.close();
        }
    }

yupengj avatar Mar 12 '24 03:03 yupengj

I am not able to reproduce this issue, and Z3 works fine for the given example.

Can you give more details about your system, such as:

  • Windows, Linux, or Mac? 32-bit or 64-bit?
  • Is another instance/library of Z3 installed system-wide?
  • Does your SmtSolverUtil introduce any unexpected options? What does this class do?
  • Does this also happen for other queries or only for the given example?

kfriedberger avatar Mar 16 '24 14:03 kfriedberger

Closing inactive issue.

kfriedberger avatar Jan 26 '25 07:01 kfriedberger