RUNNING APROVE
filename: svcomp_ex2.c.pass1.llvm
Aborted 1599095535Exec. 2, LLVMToSEGraph with some error. Reason: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Unsupported non-linear arithmetic.
            de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.assertTerm(SMTInterpol.java:918)
            aprove.Framework.SMT.Solver.SMTInterpol.SMTInterpolIntSolver.addAssertion(SMTInterpolIntSolver.java:163)
            aprove.Framework.IntegerReasoning.PlainIntegerRelationState.checkRelationWithSMTSolver(PlainIntegerRelationState.java:41)
            aprove.InputModules.Programs.llvm.internalStructures.LLVMIntegerState.checkRelation(LLVMIntegerState.java:156)
            aprove.InputModules.Programs.llvm.internalStructures.LLVMDefaultIntegerState.checkRelation(LLVMDefaultIntegerState.java:336)
            aprove.InputModules.Programs.llvm.states.LLVMAbstractState.checkRelation(LLVMAbstractState.java:469)
            aprove.InputModules.Programs.llvm.internalStructures.instructions.LLVMICmpInstruction.evaluate(LLVMICmpInstruction.java:421)
            aprove.InputModules.Programs.llvm.states.LLVMAbstractState.evaluate(LLVMAbstractState.java:540)
            aprove.InputModules.Programs.llvm.segraph.graphConstructionSteps.LLVMStandardStep.perform(LLVMStandardStep.java:98)
            aprove.InputModules.Programs.llvm.segraph.LLVMSEGraph.executeStepAndPutSucessorStepsInQueue(LLVMSEGraph.java:1089)
            aprove.InputModules.Programs.llvm.segraph.LLVMSEGraph.buildFullGraph(LLVMSEGraph.java:243)
            aprove.InputModules.Programs.llvm.segraph.LLVMSEGraph.buildFullGraph(LLVMSEGraph.java:216)
            aprove.InputModules.Programs.llvm.segraph.LLVMGraphBuilder.buildGraph(LLVMGraphBuilder.java:84)
            aprove.InputModules.Programs.llvm.processors.LLVMToSEGraphProcessor.process(LLVMToSEGraphProcessor.java:112)
            aprove.Strategies.ExecutableStrategies.Executor.execute(Executor.java:326)
            aprove.Strategies.ExecutableStrategies.Executor$Runner.wrappedRun(Executor.java:377)
            aprove.Strategies.Abortions.PooledJob.run(PooledJob.java:99)
            aprove.Strategies.Util.PrioritizableThreadPool$Worker.run(PrioritizableThreadPool.java:274)
            java.lang.Thread.run(Thread.java:748)
de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Unsupported non-linear arithmetic
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.assertTerm(SMTInterpol.java:918)
	at aprove.Framework.SMT.Solver.SMTInterpol.SMTInterpolIntSolver.addAssertion(SMTInterpolIntSolver.java:163)
	at aprove.Framework.IntegerReasoning.PlainIntegerRelationState.checkRelationWithSMTSolver(PlainIntegerRelationState.java:41)
	at aprove.InputModules.Programs.llvm.internalStructures.LLVMIntegerState.checkRelation(LLVMIntegerState.java:156)
	at aprove.InputModules.Programs.llvm.internalStructures.LLVMDefaultIntegerState.checkRelation(LLVMDefaultIntegerState.java:336)
	at aprove.InputModules.Programs.llvm.states.LLVMAbstractState.checkRelation(LLVMAbstractState.java:469)
	at aprove.InputModules.Programs.llvm.internalStructures.instructions.LLVMICmpInstruction.evaluate(LLVMICmpInstruction.java:421)
	at aprove.InputModules.Programs.llvm.states.LLVMAbstractState.evaluate(LLVMAbstractState.java:540)
	at aprove.InputModules.Programs.llvm.segraph.graphConstructionSteps.LLVMStandardStep.perform(LLVMStandardStep.java:98)
	at aprove.InputModules.Programs.llvm.segraph.LLVMSEGraph.executeStepAndPutSucessorStepsInQueue(LLVMSEGraph.java:1089)
	at aprove.InputModules.Programs.llvm.segraph.LLVMSEGraph.buildFullGraph(LLVMSEGraph.java:243)
	at aprove.InputModules.Programs.llvm.segraph.LLVMSEGraph.buildFullGraph(LLVMSEGraph.java:216)
	at aprove.InputModules.Programs.llvm.segraph.LLVMGraphBuilder.buildGraph(LLVMGraphBuilder.java:84)
	at aprove.InputModules.Programs.llvm.processors.LLVMToSEGraphProcessor.process(LLVMToSEGraphProcessor.java:112)
	at aprove.Strategies.ExecutableStrategies.Executor.execute(Executor.java:326)
	at aprove.Strategies.ExecutableStrategies.Executor$Runner.wrappedRun(Executor.java:377)
	at aprove.Strategies.Abortions.PooledJob.run(PooledJob.java:99)
	at aprove.Strategies.Util.PrioritizableThreadPool$Worker.run(PrioritizableThreadPool.java:274)
	at java.lang.Thread.run(Thread.java:748)

real	0m0.881s
user	0m1.501s
sys	0m0.164s