diff --git a/tests/aimos.t b/tests/aimos.t
new file mode 100644
index 0000000000000000000000000000000000000000..db58028220ce32fbac54817ff7734de7a61ea301
--- /dev/null
+++ b/tests/aimos.t
@@ -0,0 +1,25 @@
+Test verify
+  $ cat - > test_data.csv << EOF
+  > 4.000000000000000000e+02,4.000000000000000222e-01,-3.139370431367570990e+00,2.333333333333333428e+02,0.000000000000000000e+00
+  > 2.500000000000000000e+02,2.000000000000000111e-01,-3.138814875812015348e+00,2.333333333333333428e+02,0.000000000000000000e+00
+  > 2.500000000000000000e+02,2.222222222222222376e-01,-3.138814875812015348e+00,2.333333333333333428e+02,0.000000000000000000e+00
+  > EOF
+
+  $ chmod u+x bin/aimos
+
+  $ bin/aimos --version
+  AIMOS 1.0
+
+  $ PATH=$(pwd)/bin:$PATH
+
+  $ caisar verify -L . --format whyml --prover=AIMOS --dataset=test_data.csv - 2>&1 <<EOF
+  > theory ACASXU_P5
+  >   use TestNetwork.AsArray
+  >   use ieee_float.Float64
+  >   use caisar.DatasetClassification
+  >   use caisar.DatasetClassificationProps
+  > 
+  >   goal G: meta_robust model dataset (1.0:t)
+  > end
+  > EOF
+  [caisar] Goal G: Valid
diff --git a/tests/autodetect.t b/tests/autodetect.t
index 36d66f12046ac5df419dc6a0e4444422522eeb9c..702408e7b889e4709ef011732db70c86728eba9d 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -4,7 +4,7 @@ Test autodetect
   > echo "2.4.0"
   > EOF
 
-  $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver bin/cvc5 bin/nnenum.sh
+  $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver bin/aimos bin/cvc5 bin/nnenum.sh
 
   $ bin/alt-ergo
   2.4.0
@@ -18,6 +18,9 @@ Test autodetect
   $ bin/saver --version
   v1.0
 
+  $ bin/aimos --version
+  AIMOS 1.0
+
   $ bin/cvc5 --version
   This is cvc5 version 1.0.2 [git tag 1.0.2 branch HEAD]
 
@@ -31,6 +34,7 @@ Test autodetect
   [caisar][DEBUG] Automatic detection
   <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
   <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/aimos --version) > $TMPFILE 2>&1
   <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
   <autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
   <autodetect>Run: ($TESTCASE_ROOT/bin/nnenum.sh --version) > $TMPFILE 2>&1
@@ -45,8 +49,10 @@ Test autodetect
   <autodetect>Found prover PyRAT version 1.1 (alternative: ACAS)
   <autodetect>Found prover nnenum version dummy, OK.
   <autodetect>Found prover SAVer version v1.0, OK.
-  <autodetect>8 prover(s) added
-  [caisar] Alt-Ergo 2.4.0
+  <autodetect>Found prover AIMOS version 1.0, OK.
+  <autodetect>9 prover(s) added
+  [caisar] AIMOS 1.0
+           Alt-Ergo 2.4.0
            CVC5 1.0.2
            Marabou 1.0.+
            PyRAT 1.1
diff --git a/tests/bin/aimos b/tests/bin/aimos
new file mode 100644
index 0000000000000000000000000000000000000000..a2ef03af4319c38a7c426e226a118913d732dd53
--- /dev/null
+++ b/tests/bin/aimos
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+
+case $1 in
+    --version)
+        echo "AIMOS 1.0"
+        ;;
+    *)
+        echo "Goal:"
+        cat $2
+        echo "ACASXU_1_1.nnet, reluplex_rotation, 1.0"
+esac
diff --git a/tests/dune b/tests/dune
index d9400d21f51313cecd44a60f328da1b9f04b6ca2..26d29551ce04dff1407fd7b9534efbadc0354950 100644
--- a/tests/dune
+++ b/tests/dune
@@ -7,6 +7,7 @@
   bin/pyrat.py
   bin/Marabou
   bin/saver
+  bin/aimos
   bin/cvc5
   bin/nnenum.sh
   filter_tmpdir.sh)