% operator is supported by the theory solver that i used (z3 solver). But when i want to do mixed-concrete solving because of other non-linear constraints, i receive an error message like this:
java.lang.RuntimeException: ## Error: BinaryNonLinearSolution solution: l 6506792832578777649 op % r 5
at gov.nasa.jpf.symbc.numeric.BinaryNonLinearIntegerExpression.solution(BinaryNonLinearIntegerExpression.java:73)
at gov.nasa.jpf.symbc.concolic.PCAnalyzer.getExpression(PCAnalyzer.java:360)
at gov.nasa.jpf.symbc.concolic.PCAnalyzer.traverseConstraint(PCAnalyzer.java:383)
at gov.nasa.jpf.symbc.concolic.PCAnalyzer.createSimplifiedPC(PCAnalyzer.java:406)
at gov.nasa.jpf.symbc.concolic.PCAnalyzer.mixedIsSatisfiable(PCAnalyzer.java:54)
at gov.nasa.jpf.symbc.concolic.PCAnalyzer.isSatisfiable(PCAnalyzer.java:93)
at gov.nasa.jpf.symbc.numeric.PathCondition.simplifyOld(PathCondition.java:382)
at gov.nasa.jpf.symbc.numeric.PathCondition.simplify(PathCondition.java:331)
at gov.nasa.jpf.symbc.bytecode.AALOAD.execute(AALOAD.java:106)
at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
at gov.nasa.jpf.search.Search.forward(Search.java:579)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
at gov.nasa.jpf.JPF.run(JPF.java:613)
at gov.nasa.jpf.JPF.start(JPF.java:189)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(Method.java:498)
at gov.nasa.jpf.tool.Run.call(Run.java:80)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
% operator is supported by the theory solver that i used (z3 solver). But when i want to do mixed-concrete solving because of other non-linear constraints, i receive an error message like this:
java.lang.RuntimeException: ## Error: BinaryNonLinearSolution solution: l 6506792832578777649 op % r 5 at gov.nasa.jpf.symbc.numeric.BinaryNonLinearIntegerExpression.solution(BinaryNonLinearIntegerExpression.java:73) at gov.nasa.jpf.symbc.concolic.PCAnalyzer.getExpression(PCAnalyzer.java:360) at gov.nasa.jpf.symbc.concolic.PCAnalyzer.traverseConstraint(PCAnalyzer.java:383) at gov.nasa.jpf.symbc.concolic.PCAnalyzer.createSimplifiedPC(PCAnalyzer.java:406) at gov.nasa.jpf.symbc.concolic.PCAnalyzer.mixedIsSatisfiable(PCAnalyzer.java:54) at gov.nasa.jpf.symbc.concolic.PCAnalyzer.isSatisfiable(PCAnalyzer.java:93) at gov.nasa.jpf.symbc.numeric.PathCondition.simplifyOld(PathCondition.java:382) at gov.nasa.jpf.symbc.numeric.PathCondition.simplify(PathCondition.java:331) at gov.nasa.jpf.symbc.bytecode.AALOAD.execute(AALOAD.java:106) at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908) at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859) at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765) at gov.nasa.jpf.vm.VM.forward(VM.java:1722) at gov.nasa.jpf.search.Search.forward(Search.java:579) at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79) at gov.nasa.jpf.JPF.run(JPF.java:613) at gov.nasa.jpf.JPF.start(JPF.java:189) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62) at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) at java.lang.reflect.Method.invoke(Method.java:498) at gov.nasa.jpf.tool.Run.call(Run.java:80) at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)