Skip to content

Commit

Permalink
Do not hardcode Dynlink error in test output
Browse files Browse the repository at this point in the history
Fixes #1047
  • Loading branch information
bclement-ocp committed Mar 13, 2024
1 parent a91e98e commit 4838cfc
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions tests/cram.t/run.t
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
$ echo '(check-sat)' | alt-ergo --inequalities-plugin does-not-exist -i smtlib2 -o smtlib2 2>&1 >/dev/null | sed -E 's/\(\\".*\\"\)//'
$ echo '(check-sat)' | alt-ergo --inequalities-plugin does-not-exist -i smtlib2 -o smtlib2 2>&1 >/dev/null | sed -E 's/(error loading shared library):.*/\1/'
alt-ergo: ; Fatal Error: [Dynlink] Loading the 'inequalities' reasoner (FM module) plugin in "does-not-exist" failed!
>> Failure message: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure")
>> Failure message: error loading shared library

Now we will have some tests for the models. Note that it is okay if the format
changes slightly, you should be concerned with ensuring the semantic is
Expand Down

0 comments on commit 4838cfc

Please sign in to comment.