tamarin-prover can't run oracle

[mob0226]

When I run the following command,
tamarin-prover --prove --heuristic=O --oraclename=myoracle oracle_test.spthy
I get the following problem
tamarin-prover: ./myoracle: readCreateProcess: posix_spawnp: does not exist (No such file or directory)
myoracle is in the current folder.
Thanks.

Command line output

ubuntu@ubuntu-KVM:/Tamarin$ ls
client_session_key.aes DH.spthy myoracle oracle_test.spthy
ubuntu@ubuntu-KVM:/Tamarin$ tamarin-prover --prove=uniqueness --heuristic=O --oraclename=myoracle oracle_test.spthy
maude tool: 'maude'
checking version: 2.7.1. OK.
checking installation: OK.
[Saturating Sources] Step 1/5
[Saturating Sources] Step 2/5
[Saturating Sources] Step 1/5
[Saturating Sources] Step 2/5
[Saturating Sources] Step 1/5
[Saturating Sources] Step 2/5
tamarin-prover: ./myoracle: readCreateProcess: posix_spawnp: does not exist (No such file or directory)

[cascremers]

Hi, please have a look at #577 and see if that solves your problem.

[mob0226]

Hi, please have a look at #577 and see if that solves your problem.

Hi，I have tried to modify the Python version and checked the executable permissions of the file, but the issue has not been resolved yet. The problem I encountered is somewhat different from #577

tamarin-prover: ./myoracle: readCreateProcess: posix_spawnp: does not exist (No such file or directory)

[rsasse]

Is the file set to be executable? That is, what does a ls -la show? You can also just chmod u+x myoracle, to make it executable.

[mob0226]

Is the file set to be executable? That is, what does a ls -la show? You can also just chmod u+x myoracle, to make it executable.

Thanks.
The permissions for the file are as follows
-rwxrwxrwx 1 root root myoracle -rwxrwxrwx 1 root root oracle_test.spthy

But the issue has not been resolved yet.

[mob0226]

I'm wondering if it's related to this function posix_spawnp, but I don't know how to solve it

[rsasse]

Can you run the oracle file directly? I.e., ./myoracle in that folder? What happens?

Also, please check in your .spthy file that you do not have an oracle with a different name specified there.

[mob0226]

Can you run the oracle file directly? I.e., ./myoracle in that folder? What happens?

Also, please check in your .spthy file that you do not have an oracle with a different name specified there.

Yes, it can successfully run the myoracle file.
I runned the oracle example in Tamarin-manual and commenting on theoracle in the .spthy file, using it directly from the command line.