Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Open
yupengj opened this issue Mar 12, 2024 · 1 comment
Open

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

yupengj opened this issue Mar 12, 2024 · 1 comment
Labels
help wanted Z3

Comments

@yupengj
Copy link

yupengj commented Mar 12, 2024

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 yupengj changed the title ProverEnvironment pop Later, the variable will be incorrectly modified to be invalid argument. version 4.1.0 ProverEnvironment pop Later, the variable will be incorrectly modified to be invalid argument. Z Mar 12, 2024
@yupengj yupengj changed the title ProverEnvironment pop Later, the variable will be incorrectly modified to be invalid argument. Z ProverEnvironment pop Later, the variable will be incorrectly modified to be invalid argument. Z3 Mar 12, 2024
@kfriedberger
Copy link
Member

kfriedberger commented Mar 16, 2024 •
edited
Loading

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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
help wanted Z3
Milestone
No milestone
Development

No branches or pull requests
2 participants
@kfriedberger @yupengj