diff --git a/tests/goal.t b/tests/goal.t
new file mode 100644
index 0000000000000000000000000000000000000000..dffe78194c9f1de425276e8966c0512677487fe8
--- /dev/null
+++ b/tests/goal.t
@@ -0,0 +1,85 @@
+Test verify
+  $ . ./setup_env.sh
+
+  $ bin/Marabou --version
+  1.0.+
+
+  $ cat > file.mlw <<EOF
+  > theory T1
+  >   use ieee_float.Float64
+  >   use bool.Bool
+  >   use int.Int
+  >   use interpretation.Vector
+  >   use interpretation.NeuralNetwork
+  > 
+  >   constant nn: nn = read_neural_network "TestNetwork.nnet" NNet
+  > 
+  >   goal G1:
+  >     forall i: vector t.
+  >       has_length i 5 ->
+  >       (0.0:t) .<= i[0] .<= (0.5:t) ->
+  >       (0.0:t) .< (nn@@i)[0] .< (0.5:t)
+  > 
+  >   goal H1:
+  >     forall i: vector t.
+  >       has_length i 5 ->
+  >       (0.0:t) .<= i[0] .<= (0.5:t) /\ (0.5:t) .<= i[1] .<= (1.0:t) ->
+  >       ((0.0:t) .< (nn@@i)[0] \/ (0.5:t) .< (nn@@i)[0]) /\ (0.0:t) .< (nn@@i)[1] .< (0.5:t)
+  > 
+  >   goal I1:
+  >     forall i: vector t.
+  >       has_length i 5 ->
+  >       (0.0:t) .<= i[0] .<= (0.5:t) /\ (0.5:t) .<= i[1] .<= (1.0:t) ->
+  >       (nn@@i)[1] .< (nn@@i)[0] \/ (nn@@i)[0] .< (nn@@i)[1]
+  > 
+  >   goal J1:
+  >     forall i: vector t.
+  >       has_length i 5 ->
+  >       ((0.0:t) .<= i[0] .<= (0.5:t) \/ (0.75:t) .<= i[0] .<= (1.0:t)) /\ (0.5:t) .<= i[1] .<= (1.0:t) ->
+  >       (nn@@i)[1] .< (nn@@i)[0] \/ (nn@@i)[0] .< (nn@@i)[1]
+  > end
+  > theory T2
+  >   use ieee_float.Float64
+  >   use bool.Bool
+  >   use int.Int
+  >   use interpretation.Vector
+  >   use interpretation.NeuralNetwork
+  > 
+  >   constant nn: nn = read_neural_network "TestNetwork.nnet" NNet
+  > 
+  >   goal G2:
+  >     forall i: vector t.
+  >       has_length i 5 ->
+  >       (0.0:t) .<= i[0] .<= (0.5:t) ->
+  >       (0.0:t) .< (nn@@i)[0] .< (0.5:t)
+  > 
+  >   goal H2:
+  >     forall i: vector t.
+  >       has_length i 5 ->
+  >       (0.0:t) .<= i[0] .<= (0.5:t) /\ (0.5:t) .<= i[1] .<= (1.0:t) ->
+  >       ((0.0:t) .< (nn@@i)[0] \/ (0.5:t) .< (nn@@i)[0]) /\ (0.0:t) .< (nn@@i)[1] .< (0.5:t)
+  > 
+  >   goal I2:
+  >     forall i: vector t.
+  >       has_length i 5 ->
+  >       (0.0:t) .<= i[0] .<= (0.5:t) /\ (0.5:t) .<= i[1] .<= (1.0:t) ->
+  >       (nn@@i)[1] .< (nn@@i)[0] \/ (nn@@i)[0] .< (nn@@i)[1]
+  > 
+  >   goal J2:
+  >     forall i: vector t.
+  >       has_length i 5 ->
+  >       ((0.0:t) .<= i[0] .<= (0.5:t) \/ (0.75:t) .<= i[0] .<= (1.0:t)) /\ (0.5:t) .<= i[1] .<= (1.0:t) ->
+  >       (nn@@i)[1] .< (nn@@i)[0] \/ (nn@@i)[0] .< (nn@@i)[1]
+  > end
+  > EOF
+
+  $ caisar verify --prover=Marabou -g T1:G1 file.mlw 2>&1 | ./filter_tmpdir.sh
+  Goal G1: Unknown ()
+  Goal G2: Unknown ()
+  Goal H2: Unknown ()
+  Goal I2: Unknown ()
+  Goal J2: Unknown ()
+
+  $ caisar verify --prover=Marabou -g T1: -g T2:H2,J2 file.mlw 2>&1 | ./filter_tmpdir.sh
+  Goal H2: Unknown ()
+  Goal J2: Unknown ()