summaryrefslogtreecommitdiff
path: root/config
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2014-03-07 18:00:37 -0500
committerTim King <taking@cs.nyu.edu>2014-03-07 18:00:52 -0500
commit9ccdea06edbc72e3ecd282e9e015f6fc4b2e7173 (patch)
treecde6138cb9ab6ef0b7c15edf42e3e8cc53637002 /config
parent42be934ef4d4430944ae9074c7202a7d130c75bb (diff)
Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.
Diffstat (limited to 'config')
-rw-r--r--config/glpk.m44
1 files changed, 2 insertions, 2 deletions
diff --git a/config/glpk.m4 b/config/glpk.m4
index 6c59a3094..932b053e0 100644
--- a/config/glpk.m4
+++ b/config/glpk.m4
@@ -95,7 +95,7 @@ if test -z "$GLPK_LIBS"; then
[#else]
[#include <glpk.h>]
[#endif],
- [int i = lpx_get_int_parm(NULL, LPX_K_ITCNT)])],
+ [int i = glp_get_it_cnt(NULL)])],
[GLPK_LIBS="-lglpk $1"],
[])
LIBS="$cvc4_save_LIBS"
@@ -118,7 +118,7 @@ if test -z "$GLPK_LIBS"; then
[#else]
[#include <glpk.h>]
[#endif],
- [int i = lpx_get_int_parm(NULL, LPX_K_ITCNT)])],
+ [int i = glp_get_it_cnt(NULL)])],
[GLPK_LIBS="-lglpk $1"],
[])
LIBS="$cvc4_save_LIBS"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback